dotnet-console-interview-example/spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla at main · SignalRichard/dotnet-console-interview-example · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
------------------- MODULE RemoveSingleInstanceCharacters -------------------

EXTENDS Integers, Sequences, TLC

(*
--algorithm RemoveSingleInstanceCharacters {
    variables antepenultimate, previous, current = "",
        singleInstance = { "0" },
        i = 1,
        input = << >>, result = << >>,
        domainSize \in 1..5,
        domain \in [1..domainSize -> 1..2],
        characterMapping = << "a", "0" >>;

    {
        while(i =< Len(domain)) {
            input := Append(input, characterMapping[domain[i]]);
            i := i + 1;
        };

        i := 1;

        while(i =< Len(input)) {
            current := input[i];

            if(~(previous = "")) {
              if(~({ previous } \subseteq singleInstance) \/ ({ current } \subseteq singleInstance)) {
                    result := Append(result, previous);
                };
                else {
                    if({ antepenultimate } \subseteq singleInstance) {
                        result := Append(result, previous);
                    };
                };
            };

            antepenultimate := previous;
            previous := current;
            current := "";
            i := i + 1;
        };

        if(~(previous = "")) {
          if(~({ previous } \subseteq singleInstance) \/ ({ current } \subseteq singleInstance)) {
                result := Append(result, previous);
            };
            else {
                if({ antepenultimate } \subseteq singleInstance) {
                    result := Append(result, previous);
                };
            };
        };

        assert \A n \in 1..Len(result) : \/ ~({ result[n] } \subseteq singleInstance)
                                         \/ ({ result[n] } \subseteq singleInstance) /\ ((n - 1 >= 1 /\ { result[n - 1] } \subseteq singleInstance) \/ (n + 1 <= Len(result) /\ { result[n + 1] } \subseteq singleInstance));
    }
}
*)
\* BEGIN TRANSLATION (chksum(pcal) = "586bf200" /\ chksum(tla) = "5c7b1f60")
CONSTANT defaultInitValue
VARIABLES pc, antepenultimate, previous, current, singleInstance, i, input,
          result, domainSize, domain, characterMapping

vars == << pc, antepenultimate, previous, current, singleInstance, i, input,
           result, domainSize, domain, characterMapping >>

Init == (* Global variables *)
        /\ antepenultimate = defaultInitValue
        /\ previous = defaultInitValue
        /\ current = ""
        /\ singleInstance = { "0" }
        /\ i = 1
        /\ input = << >>
        /\ result = << >>
        /\ domainSize \in 1..5
        /\ domain \in [1..domainSize -> 1..2]
        /\ characterMapping = << "a", "0" >>
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ IF i =< Len(domain)
               THEN /\ input' = Append(input, characterMapping[domain[i]])
                    /\ i' = i + 1
                    /\ pc' = "Lbl_1"
               ELSE /\ i' = 1
                    /\ pc' = "Lbl_2"
                    /\ input' = input
         /\ UNCHANGED << antepenultimate, previous, current, singleInstance,
                         result, domainSize, domain, characterMapping >>

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF i =< Len(input)
               THEN /\ current' = input[i]
                    /\ IF ~(previous = "")
                          THEN /\ IF ~({ previous } \subseteq singleInstance) \/ ({ current' } \subseteq singleInstance)
                                     THEN /\ result' = Append(result, previous)
                                     ELSE /\ IF { antepenultimate } \subseteq singleInstance
                                                THEN /\ result' = Append(result, previous)
                                                ELSE /\ TRUE
                                                     /\ UNCHANGED result
                          ELSE /\ TRUE
                               /\ UNCHANGED result
                    /\ antepenultimate' = previous
                    /\ previous' = current'
                    /\ pc' = "Lbl_3"
               ELSE /\ IF ~(previous = "")
                          THEN /\ IF ~({ previous } \subseteq singleInstance) \/ ({ current } \subseteq singleInstance)
                                     THEN /\ result' = Append(result, previous)
                                     ELSE /\ IF { antepenultimate } \subseteq singleInstance
                                                THEN /\ result' = Append(result, previous)
                                                ELSE /\ TRUE
                                                     /\ UNCHANGED result
                          ELSE /\ TRUE
                               /\ UNCHANGED result
                    /\ Assert(\A n \in 1..Len(result') : \/ ~({ result'[n] } \subseteq singleInstance)
                                                         \/ ({ result'[n] } \subseteq singleInstance) /\ ((n - 1 >= 1 /\ { result'[n - 1] } \subseteq singleInstance) \/ (n + 1 <= Len(result') /\ { result'[n + 1] } \subseteq singleInstance)),
                              "Failure of assertion at line 54, column 9.")
                    /\ pc' = "Done"
                    /\ UNCHANGED << antepenultimate, previous, current >>
         /\ UNCHANGED << singleInstance, i, input, domainSize, domain,
                         characterMapping >>

Lbl_3 == /\ pc = "Lbl_3"
         /\ current' = ""
         /\ i' = i + 1
         /\ pc' = "Lbl_2"
         /\ UNCHANGED << antepenultimate, previous, singleInstance, input,
                         result, domainSize, domain, characterMapping >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1 \/ Lbl_2 \/ Lbl_3
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

=============================================================================
\* Modification History
\* Last modified Mon Nov 03 22:22:15 EST 2025 by rbolh
\* Created Mon Nov 03 22:20:02 EST 2025 by rbolh