diff --git a/general/docs/contributions.md b/general/docs/contributions.md
index d9a8143dfe1fe085b0c6b1210e158a290385e861..03e1ac8003413b8250e64f36f0f89a6f506c65eb 100644
--- a/general/docs/contributions.md
+++ b/general/docs/contributions.md
@@ -27,7 +27,18 @@ The TLC process can be long running. It possibly runs for days, weeks or months.
TLAPS
-----
-TBD
+#### Automatic expansion of operator definitions (difficulty: moderate) (skills: OCaml)
+
+TLAPS currently relies on the user to indicate which operator definitions should be expanded before calling the back-end provers. Forgetting to expand an operator may make an obligation unprovable, expanding too many operators may result in a search space too big for the back-end to handle. The objective of this work would be to automatically detect which definitions have to be expanded, based on iterative deepening and possibly heuristics on the occurrences of operators in the context. The method could return the list of expanded operators so that it can be inserted in the proof, eschewing the need for repeating the search when the proof is rerun. Doing so requires modifying the proof manager but not the individual back-end interfaces.
+
+#### SMT support for reasoning about regular expressions (difficulty: moderate to high) (skills: OCaml, SMT, TLA+)
+
+Reasoning about TLA+ sequences currently mainly relies on the lemmas provided in the module SequenceTheorems and therefore comes with very little automation. Certain SMT solvers including [Z3](https://sites.google.com/site/z3strsolver/) and [CVC4](https://github.com/CVC4/CVC4) include support for reasoning about strings and regular expressions. Integrating these capabilities in TLAPS would be useful, for example when reasoning about the contents of message channels in distributed algorithms. Doing so will require extending the SMT backend of TLAPS, including its underlying type checker for recognizing regular expressions, represented using custom TLA+ operators.
+
+#### Generate counter-examples for invalid proof obligations (difficulty: moderate to high) (skills: OCaml, TLA+)
+
+Most conjectures that users attempt to prove during proof development are in fact not valid. For example, hypotheses needed to prove a step are not provided to the prover, the invariant may not be strong enough etc. When this is the case, the back-end provers time out but do not provide any useful information to the user. The objective of this work is to connect a model generator such as [Nunchaku](https://github.com/nunchaku-inria/nunchaku) to TLAPS that could provide an explanation to the user why the proof obligation is not valid. The main difficulty will be defining a translation from a useful sublanguage of TLA+ set-theoretic expressions to the input language of Nunchaku, which resembles a functional programming language.
+
TLA Toolbox
-----------
diff --git a/general/performance/EWD840/EWD840.tla b/general/performance/EWD840/EWD840.tla
new file mode 100644
index 0000000000000000000000000000000000000000..1222f26ceb06fc5f3856cd0fdf03bd0fa41b0a0a
--- /dev/null
+++ b/general/performance/EWD840/EWD840.tla
@@ -0,0 +1,142 @@
+
+------------------------------- MODULE EWD840 -------------------------------
+
+EXTENDS Naturals
+
+CONSTANT N
+ASSUME NAssumption == N \in Nat \ {0}
+
+VARIABLES active, color, tpos, tcolor
+vars == <<active, color, tpos, tcolor>>
+
+Nodes == 0 .. N-1
+Color == {"white", "black"}
+
+TypeOK ==
+ /\ active \in [Nodes -> BOOLEAN] \* status of nodes (active or passive)
+ /\ color \in [Nodes -> Color] \* color of nodes
+ /\ tpos \in Nodes \* token position
+ /\ tcolor \in Color \* token color
+
+(* Initially the token is at node 0, and it is black. There
+ are no constraints on the status and color of the nodes. *)
+Init ==
+ /\ active \in [Nodes -> BOOLEAN] \* Array of nodes to boolean mappings, initially all false
+ /\ color \in [Nodes -> Color] \* Array of nodes to (node) color mappings, initially all white
+ /\ tpos = 0
+ /\ tcolor = "black"
+
+(* Node 0 may initiate a probe when it has the token and
+ when either it is black or the token is black. This is
+ necessary to terminate once a conclusive round has ended.
+ It passes a white token to node N-1 and paints itself white. *)
+InitiateProbe ==
+ /\ tpos = 0 \* Initially the token is a the 0 node
+ /\ tcolor = "black" \/ color[0] = "black" \* Prevent the master node from starting another round after it has received a positive result (termination) in the previous round.
+ \* Note that TLC will terminate even without this condition, it won't show algorithm termination represented by a deadlock though.
+ /\ tpos' = N-1 \* In the next state the token is at node N-1
+ /\ tcolor' = "white" \* In the next state the token color is white
+ /\ color' = [color EXCEPT ![0] = "white"] \* node colors are preserved/unchanged, except of node 0 (who initiated the probe)
+ /\ UNCHANGED <<active>> \* The active states are preservered/unchanged in the next state
+
+(* A node i different from 0 that possesses the token may pass
+ it to node i-1 under the following circumstances:
+ - node i is inactive or
+ - node i is colored black or
+ - the token is black.
+ Note that the last two conditions will result in an
+ inconclusive round, since the token will be black.
+ The token will be stained if node i is black, otherwise
+ its color is unchanged. Node i will be made white. *)
+PassToken(i) ==
+ /\ tpos = i \* Node i can only pass the token if it posses it
+ /\ ~ active[i] \* Node i is inactive
+ \/ color[i] = "black" \* Node i has been marked stained already
+ \/ tcolor = "black" \* The token has been stained by a higher node already
+ /\ tpos' = i-1
+ /\ tcolor' = IF color[i] = "black" THEN "black" ELSE tcolor
+ /\ color' = [color EXCEPT ![i] = "white"]
+ /\ UNCHANGED <<active>>
+
+(* An active node i may activate another node j by sending it
+ a message. If j>i (hence activation goes against the direction
+ of the token being passed), then node i becomes black. *)
+SendMsg(i) ==
+ /\ active[i] \* Only allowed to send msgs if node i is active
+ /\ \E j \in Nodes \ {i} :
+ /\ active' = [active EXCEPT ![j] = TRUE]
+ /\ color' = [color EXCEPT ![i] = IF j>i THEN "black" ELSE @]
+ /\ UNCHANGED <<tpos, tcolor>>
+
+(* Any active node may become inactive at any moment. *)
+Deactivate(i) ==
+ /\ active[i]
+ /\ active' = [active EXCEPT ![i] = FALSE]
+ /\ UNCHANGED <<color, tpos, tcolor>>
+
+(* next-state relation: disjunction of above actions *)
+Next ==
+ \/ InitiateProbe
+ \/ \E i \in Nodes \ {0} : PassToken(i)
+ \/ \E i \in Nodes : SendMsg(i) \/ Deactivate(i)
+
+(* Actions controlled by termination detection algorithm *)
+System ==
+ \/ InitiateProbe
+ \/ \E i \in Nodes \ {0} : PassToken(i)
+
+Fairness == WF_vars(System)
+
+Spec == Init /\ [][Next]_vars /\ Fairness
+
+LInv == [][Next]_vars => WF_vars(System)
+
+-----------------------------------------------------------------------------
+
+(***************************************************************************)
+(* Non-invariants that can be used for validating the specification. *)
+(***************************************************************************)
+NeverBlack == \A i \in Nodes : color[i] # "black"
+
+NeverChangeColor == [][ \A i \in Nodes : UNCHANGED color[i] ]_vars
+
+(***************************************************************************)
+(* Main safety property: if there is a white token at node 0 then every *)
+(* node is inactive. *)
+(***************************************************************************)
+terminationDetected ==
+ /\ tpos = 0 /\ tcolor = "white"
+ /\ color[0] = "white" /\ ~ active[0]
+ /\ color[1] = "white"
+
+TerminationDetection ==
+ terminationDetected => \A i \in Nodes : ~ active[i]
+(***************************************************************************)
+(* Liveness property: termination is eventually detected. *)
+(***************************************************************************)
+Liveness ==
+ /\ (\A i \in Nodes : ~ active[i]) ~> terminationDetected
+
+(***************************************************************************)
+(* The following property says that eventually all nodes will terminate *)
+(* assuming that from some point onwards no messages are sent. It is *)
+(* undesired, but verified for the fairness condition WF_vars(Next). *)
+(* This motivates weakening the fairness condition to WF_vars(System). *)
+(***************************************************************************)
+AllNodesTerminateIfNoMessages ==
+ <>[][~ \E i \in Nodes : SendMsg(i)]_vars
+ => <>(\A i \in Nodes : ~ active[i])
+
+(***************************************************************************)
+(* Dijkstra's inductive invariant *)
+(***************************************************************************)
+Inv ==
+ \/ P0:: \A i \in Nodes : tpos < i => ~ active[i]
+ \/ P1:: \E j \in 0 .. tpos : color[j] = "black"
+ \/ P2:: tcolor = "black"
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Sep 06 18:13:33 CEST 2017 by markus
+\* Last modified Tue Jun 10 09:50:24 CEST 2014 by merz
+\* Created Mon Sep 09 11:33:10 CEST 2013 by merz
diff --git a/general/performance/EWD840/MC.cfg b/general/performance/EWD840/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..bb9482f0c119f60c0fb1348fbdb78054730a68a9
--- /dev/null
+++ b/general/performance/EWD840/MC.cfg
@@ -0,0 +1,7 @@
+\* CONSTANT definitions
+CONSTANT
+N <- const_1515403233990126000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_1515403233990127000
+\* Generated on Mon Jan 08 10:20:33 CET 2018
\ No newline at end of file
diff --git a/general/performance/EWD840/MC.tla b/general/performance/EWD840/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..d99e2d61c343e03f93f009a7f271ea4532aa4590
--- /dev/null
+++ b/general/performance/EWD840/MC.tla
@@ -0,0 +1,15 @@
+---- MODULE MC ----
+EXTENDS EWD840, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1515403233990126000 ==
+12
+----
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_1515403233990127000 ==
+Spec
+----
+=============================================================================
+\* Modification History
+\* Created Mon Jan 08 10:20:33 CET 2018 by markus
diff --git a/general/performance/PaxosMadeSimple/LICENSE.md b/general/performance/PaxosMadeSimple/LICENSE.md
new file mode 100644
index 0000000000000000000000000000000000000000..e7e634577976b0889f469f6c7e3acfa2a4b6c9a2
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/LICENSE.md
@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2015 nano-o
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/general/performance/PaxosMadeSimple/LINK.md b/general/performance/PaxosMadeSimple/LINK.md
new file mode 100644
index 0000000000000000000000000000000000000000..360a8ce7d3af5f79f9a1543fd297a0d93fc9b352
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/LINK.md
@@ -0,0 +1 @@
+Copied from https://github.com/nano-o/PaxosMadeSimple
diff --git a/general/performance/PaxosMadeSimple/MC.cfg b/general/performance/PaxosMadeSimple/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..9e9e419905f1d826a8c37cf3378e11f4e2b3cb1f
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/MC.cfg
@@ -0,0 +1,31 @@
+\* MV CONSTANT declarations
+CONSTANTS
+a1 = a1
+a2 = a2
+a3 = a3
+\* MV CONSTANT declarations
+CONSTANTS
+v1 = v1
+v2 = v2
+\* MV CONSTANT definitions
+CONSTANT
+Acceptor <- const_144139943710210000
+\* MV CONSTANT definitions
+CONSTANT
+Value <- const_144139943711311000
+\* SYMMETRY definition
+SYMMETRY symm_144139943712312000
+\* CONSTANT definitions
+CONSTANT
+Quorum <- const_144139943713313000
+\* CONSTANT definition
+CONSTANT
+None = None
+Nat <- def_ov_144139943715315000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_144139943716316000
+\* INVARIANT definition
+INVARIANT
+inv_144139943717317000
+\* Generated on Fri Sep 04 16:43:57 EDT 2015
\ No newline at end of file
diff --git a/general/performance/PaxosMadeSimple/MC.tla b/general/performance/PaxosMadeSimple/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..1e615018a4f091311de55f8b79fbf8b94da287ee
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/MC.tla
@@ -0,0 +1,48 @@
+---- MODULE MC ----
+EXTENDS PaxosMadeSimple, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+a1, a2, a3
+----
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+v1, v2
+----
+
+\* MV CONSTANT definitions Acceptor
+const_144139943710210000 ==
+{a1, a2, a3}
+----
+
+\* MV CONSTANT definitions Value
+const_144139943711311000 ==
+{v1, v2}
+----
+
+\* SYMMETRY definition
+symm_144139943712312000 ==
+Permutations(const_144139943710210000) \union Permutations(const_144139943711311000)
+----
+
+\* CONSTANT definitions @modelParameterConstants:2Quorum
+const_144139943713313000 ==
+{Q \in SUBSET Acceptor : Cardinality(Q) > Cardinality(Acceptor)\div 2}
+----
+
+\* CONSTANT definition @modelParameterDefinitions:1
+def_ov_144139943715315000 ==
+0..4
+----
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_144139943716316000 ==
+Spec
+----
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_144139943717317000 ==
+Correctness
+----
+=============================================================================
+\* Modification History
+\* Created Fri Sep 04 16:43:57 EDT 2015 by nano
diff --git a/general/performance/PaxosMadeSimple/PaxosMadeSimple.tla b/general/performance/PaxosMadeSimple/PaxosMadeSimple.tla
new file mode 100644
index 0000000000000000000000000000000000000000..2c9da130b36c500978a0850e6eefac7e119ea239
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/PaxosMadeSimple.tla
@@ -0,0 +1,311 @@
+-------------------------- MODULE PaxosMadeSimple --------------------------
+(***************************************************************************)
+(* A specification of the algorithm described in "Paxos Made Simple", *)
+(* based on the specification found in: *)
+(* `^\url{research.microsoft.com/en-us/um/people/lamport/tla/PConProof.tla}^' *)
+(***************************************************************************)
+EXTENDS Integers, FiniteSets
+-----------------------------------------------------------------------------
+
+CONSTANT Value, Acceptor, Quorum
+
+ASSUME QA == /\ \A Q \in Quorum : Q \subseteq Acceptor
+ /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 # {}
+
+(***************************************************************************)
+(* Ballot numbers are the natural numbers. *)
+(***************************************************************************)
+Ballot == Nat
+
+(***************************************************************************)
+(* We are going to have a leader PlusCal process for each ballot and an *)
+(* acceptor PlusCal process for each acceptor (see the "process" *)
+(* definitions below). A proposer that proposes a value in ballot n is *)
+(* modeled by the leader PlusCal process identified by n. Thus a single *)
+(* proposer is modeled by multiple leader PlusCal processes, one for each *)
+(* ballot in which the proposer proposes a value. We use the ballot *)
+(* numbers and the acceptors themselves as the identifiers for these *)
+(* processes and we assume that the set of ballots and the set of *)
+(* acceptors are disjoint. For good measure, we also assume that -1 is *)
+(* not an acceptor, although that is probably not necessary. *)
+(***************************************************************************)
+ASSUME BallotAssump == (Ballot \cup {-1}) \cap Acceptor = {}
+
+(***************************************************************************)
+(* We define None to be an unspecified value that is not in the set Value. *)
+(***************************************************************************)
+None == CHOOSE v : v \notin Value
+
+(***************************************************************************)
+(* This is a message-passing algorithm, so we begin by defining the set *)
+(* Message of all possible messages. The messages are explained below *)
+(* with the actions that send them. A message m with m.type = "1a" is *)
+(* called a 1a message, and similarly for the other message types. *)
+(***************************************************************************)
+Message == [type : {"1a"}, bal : Ballot]
+ \cup [type : {"1b"}, acc : Acceptor, bal : Ballot,
+ mbal : Ballot \cup {-1}, mval : Value \cup {None}]
+ \cup [type : {"2a"}, bal : Ballot, val : Value]
+ \cup [type : {"2b"}, acc : Acceptor, bal : Ballot, val : Value]
+
+-----------------------------------------------------------------------------
+
+
+(***************************************************************************)
+(* The algorithm is easiest to understand in terms of the set msgs of all *)
+(* messages that have ever been sent. A more accurate model would use one *)
+(* or more variables to represent the messages actually in transit, and it *)
+(* would include actions representing message loss and duplication as well *)
+(* as message receipt. *)
+(* *)
+(* In the current spec, there is no need to model message loss explicitly. *)
+(* The safety part of the spec says only what messages may be received and *)
+(* does not assert that any message actually is received. Thus, there is *)
+(* no difference between a lost message and one that is never received. *)
+(* The liveness property of the spec will make it clear what messages must *)
+(* be received (and hence either not lost or successfully retransmitted if *)
+(* lost) to guarantee progress. *)
+(* *)
+(* Another advantage of maintaining the set of all messages that have ever *)
+(* been sent is that it allows us to define the state function `votes' *)
+(* that implements the variable of the same name in the voting algorithm *)
+(* without having to introduce a history variable. *)
+(***************************************************************************)
+
+(***********
+
+--algorithm PCon {
+ variables maxBal = [a \in Acceptor |-> -1] ,
+ maxVBal = [a \in Acceptor |-> -1] ,
+ maxVVal = [a \in Acceptor |-> None] ,
+ msgs = {}
+ define {
+ sentMsgs(t, b) == {m \in msgs : (m.type = t) /\ (m.bal = b)}
+
+ Max(xs, LessEq(_,_)) ==
+ CHOOSE x \in xs : \A y \in xs : LessEq(y,x)
+
+ HighestAcceptedValue(Q1bMessages) ==
+ Max(Q1bMessages, LAMBDA m1,m2 : m1.mbal \leq m2.mbal).mval
+
+ (***********************************************************************)
+ (* We define ShowsSafeAt so that ShowsSafeAt(Q, b, v) is true for a *)
+ (* quorum Q iff the msgs contained in ballot-b 1b messages from the *)
+ (* acceptors in Q show that v is safe at b. *)
+ (***********************************************************************)
+ ShowsSafeAt(Q, b, v) ==
+ LET Q1b == {m \in sentMsgs("1b", b) : m.acc \in Q}
+ IN /\ \A a \in Q : \E m \in Q1b : m.acc = a
+ /\ \/ \A m \in Q1b : m.mbal = -1
+ \/ v = HighestAcceptedValue(Q1b)
+ }
+
+ (*************************************************************************)
+ (* We describe each action as a macro. *)
+ (* *)
+ (* In PlusCal, `self' is used by convention to designate the id of the *)
+ (* PlusCal process being defined. *)
+ (* *)
+ (* The leader for ballot `self' can execute a Phase1a() action, which *)
+ (* sends the ballot `self' 1a message (remember that for leader PlusCal *)
+ (* processes, the identifier of the process is the ballot number). *)
+ (*************************************************************************)
+ macro Phase1a() { msgs := msgs \cup {[type |-> "1a", bal |-> self]} ; }
+
+ (*************************************************************************)
+ (* Acceptor `self' can perform a Phase1b(b) action, which is enabled iff *)
+ (* b > maxBal[self]. The action sets maxBal[self] to b (therefore *)
+ (* promising never to accept proposals with ballot lower than b: see *)
+ (* Phase2b below) and sends a phase 1b message to the leader of ballot b *)
+ (* containing the values of maxVBal[self] and maxVVal[self]. *)
+ (*************************************************************************)
+ macro Phase1b(b) {
+ when (b > maxBal[self]) /\ (sentMsgs("1a", b) # {});
+ maxBal[self] := b;
+ msgs := msgs \cup {[type |-> "1b", acc |-> self, bal |-> b,
+ mbal |-> maxVBal[self], mval |-> maxVVal[self]]} ;
+ }
+
+ (*************************************************************************)
+ (* The ballot `self' leader can perform a Phase2a(v) action, sending a *)
+ (* 2a message for value v, if it has not already sent a 2a message (for *)
+ (* this ballot) and it can determine that v is safe at ballot `self'. *)
+ (*************************************************************************)
+ macro Phase2a(v) {
+ when /\ sentMsgs("2a", self) = {}
+ /\ \E Q \in Quorum : ShowsSafeAt(Q, self, v);
+ msgs := msgs \cup {[type |-> "2a", bal |-> self, val |-> v]};
+ }
+
+ (*************************************************************************)
+ (* The Phase2b(b) action is executed by acceptor `self' in response to a *)
+ (* ballot-b 2a message. Note this action can be executed multiple times *)
+ (* by the acceptor, but after the first one, all subsequent executions *)
+ (* are stuttering steps that do not change the value of any variable. *)
+ (* Note that the acceptor `self' does not accept any proposal with a *)
+ (* ballot lower than b, as per its promise to the leader of ballot b in *)
+ (* Phase1b above. *)
+ (* *)
+ (* Note that there is not need to update maxBal. *)
+ (*************************************************************************)
+ macro Phase2b(b) {
+ when b \geq maxBal[self] ;
+ with (m \in sentMsgs("2a", b)) {
+ if (b \geq maxVBal[self]) {
+ maxVBal[self] := b;
+ maxVVal[self] := m.val
+ };
+ msgs := msgs \cup {[type |-> "2b", acc |-> self,
+ bal |-> b, val |-> m.val]}
+ }
+ }
+
+ (*************************************************************************)
+ (* An acceptor performs the body of its `while' loop as a single atomic *)
+ (* action by nondeterministically choosing a ballot in which its Phase1b *)
+ (* or Phase2b action is enabled and executing that enabled action. If *)
+ (* no such action is enabled, the acceptor does nothing. *)
+ (*************************************************************************)
+ process (acceptor \in Acceptor) {
+ acc: while (TRUE) {
+ with (b \in Ballot) { either Phase1b(b) or Phase2b(b) } }
+ }
+
+ (*************************************************************************)
+ (* The leader of a ballot nondeterministically chooses one of its *)
+ (* actions that is enabled (and the argument for which it is enabled) *)
+ (* and performs it atomically. It does nothing if none of its actions *)
+ (* is enabled. *)
+ (*************************************************************************)
+ process (leader \in Ballot) {
+ ldr: while (TRUE) {
+ either Phase1a()
+ or with (v \in Value) { Phase2a(v) }
+ }
+ }
+
+}
+
+**********)
+
+(***************************************************************************)
+(* Below is the translation (obtained automatically) of the PlusCal *)
+(* algorithm above. *)
+(***************************************************************************)
+\* BEGIN TRANSLATION
+VARIABLES maxBal, maxVBal, maxVVal, msgs
+
+(* define statement *)
+sentMsgs(t, b) == {m \in msgs : (m.type = t) /\ (m.bal = b)}
+
+Max(xs, LessEq(_,_)) ==
+ CHOOSE x \in xs : \A y \in xs : LessEq(y,x)
+
+HighestAcceptedValue(Q1bMessages) ==
+ Max(Q1bMessages, LAMBDA m1,m2 : m1.mbal \leq m2.mbal).mval
+
+
+
+
+
+
+ShowsSafeAt(Q, b, v) ==
+ LET Q1b == {m \in sentMsgs("1b", b) : m.acc \in Q}
+ IN /\ \A a \in Q : \E m \in Q1b : m.acc = a
+ /\ \/ \A m \in Q1b : m.mbal = -1
+ \/ v = HighestAcceptedValue(Q1b)
+
+
+vars == << maxBal, maxVBal, maxVVal, msgs >>
+
+ProcSet == (Acceptor) \cup (Ballot)
+
+Init == (* Global variables *)
+ /\ maxBal = [a \in Acceptor |-> -1]
+ /\ maxVBal = [a \in Acceptor |-> -1]
+ /\ maxVVal = [a \in Acceptor |-> None]
+ /\ msgs = {}
+
+acceptor(self) == \E b \in Ballot:
+ \/ /\ (b > maxBal[self]) /\ (sentMsgs("1a", b) # {})
+ /\ maxBal' = [maxBal EXCEPT ![self] = b]
+ /\ msgs' = (msgs \cup {[type |-> "1b", acc |-> self, bal |-> b,
+ mbal |-> maxVBal[self], mval |-> maxVVal[self]]})
+ /\ UNCHANGED <<maxVBal, maxVVal>>
+ \/ /\ b \geq maxBal[self]
+ /\ \E m \in sentMsgs("2a", b):
+ /\ IF b \geq maxVBal[self]
+ THEN /\ maxVBal' = [maxVBal EXCEPT ![self] = b]
+ /\ maxVVal' = [maxVVal EXCEPT ![self] = m.val]
+ ELSE /\ TRUE
+ /\ UNCHANGED << maxVBal, maxVVal >>
+ /\ msgs' = (msgs \cup {[type |-> "2b", acc |-> self,
+ bal |-> b, val |-> m.val]})
+ /\ UNCHANGED maxBal
+
+leader(self) == /\ \/ /\ msgs' = (msgs \cup {[type |-> "1a", bal |-> self]})
+ \/ /\ \E v \in Value:
+ /\ /\ sentMsgs("2a", self) = {}
+ /\ \E Q \in Quorum : ShowsSafeAt(Q, self, v)
+ /\ msgs' = (msgs \cup {[type |-> "2a", bal |-> self, val |-> v]})
+ /\ UNCHANGED << maxBal, maxVBal, maxVVal >>
+
+Next == (\E self \in Acceptor: acceptor(self))
+ \/ (\E self \in Ballot: leader(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION
+
+(***************************************************************************)
+(* TypeOK is an invariant asserting that the variables are of the type *)
+(* that we expect. We use it to catch trivial "coding" errors. *)
+(***************************************************************************)
+TypeOK == /\ maxBal \in [Acceptor -> Ballot \cup {-1}]
+ /\ maxVBal \in [Acceptor -> Ballot \cup {-1}]
+ /\ maxVVal \in [Acceptor -> Value \cup {None}]
+ /\ msgs \subseteq Message
+
+(***************************************************************************)
+(* Chosen(b, v) is true when a quorum of acceptors have broadcasted a 2b *)
+(* message with the same value v in ballot b. Note that a learner *)
+(* (learners are not modeled in this specification) ca learn v if and only *)
+(* if Chosen(b, v) is true for some ballot b. *)
+(***************************************************************************)
+ChosenIn(b, v) ==
+ \E Q \in Quorum : \A a \in Q :
+ \E m \in sentMsgs("2b", b) :
+ /\ m.acc = a
+ /\ m.val = v
+
+(***************************************************************************)
+(* Chosen(v) is true when v has been chosen in some ballot. *)
+(***************************************************************************)
+Chosen(v) == \E b \in Ballot : ChosenIn(b,v)
+
+(***************************************************************************)
+(* The Agreement property of the consensus problem says that no two *)
+(* learners learn different values. Since a learner can learn a value v *)
+(* if and only if Chosen(v) is true, the following Correctness property *)
+(* implies Agreement. *)
+(***************************************************************************)
+Correctness ==
+ \A v1,v2 \in Value : Chosen(v1) /\ Chosen(v2) => v1 = v2
+
+(***************************************************************************)
+(* This theorem states that in every execution of the specification, the *)
+(* Correcntess property is always true. Note that in the current form of *)
+(* the spec, this theorem is incorrect. Use TLC to find an execution that *)
+(* violates it. *)
+(***************************************************************************)
+THEOREM Spec => []Correctness
+
+Votes == [a \in Acceptor |->
+ [b \in Nat |-> IF \E v \in Value : [type |-> "2b", bal |-> b, acc |-> a, val |-> v] \in msgs
+ THEN CHOOSE v \in Value : [type |-> "2b", bal |-> b, acc |-> a, val |-> v] \in msgs
+ ELSE <<>>]]
+
+=============================================================================
+\* Modification History
+\* Last modified Fri Aug 04 16:16:29 PDT 2017 by nano
+\* Created Thu Sep 03 22:58:03 EDT 2015 by nano
diff --git a/general/performance/PaxosMadeSimple/README.md b/general/performance/PaxosMadeSimple/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..e94aa6f4acf61c93500460a78edcdd0fe547b03d
--- /dev/null
+++ b/general/performance/PaxosMadeSimple/README.md
@@ -0,0 +1,11 @@
+# PaxosMadeSimple
+A TLA+ formalization of the algorithm described in "Paxos Made Simple"
+There are two specification: SimplePaxos.tla and PaxosMadeSimple.tla.
+The second one is a modification of a specification found here:
+research.microsoft.com/en-us/um/people/lamport/tla/PConProof.tla
+
+Each spec can be model-checked by opening it in the TLA toolbox and instructing the toolbox to import the model named "Model_1", then running TLC.
+
+Some people think that there is a problem in the algorithm as described in the paper:
+http://stackoverflow.com/questions/29880949/contradiction-in-lamports-paxos-made-simple-paper.
+However the accepted answer is plain wrong; there is no problem, as can be checked with TLC.
diff --git a/org.lamport.tla.toolbox.jclouds/.classpath b/org.lamport.tla.toolbox.jclouds/.classpath
index 098194ca4b7d8f45177f94e735506ae3a26b5c94..eca7bdba8f03f22510b7980a94dbfe10c16c0901 100644
--- a/org.lamport.tla.toolbox.jclouds/.classpath
+++ b/org.lamport.tla.toolbox.jclouds/.classpath
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7"/>
+ <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="bin"/>
diff --git a/org.lamport.tla.toolbox.jclouds/.settings/org.eclipse.jdt.core.prefs b/org.lamport.tla.toolbox.jclouds/.settings/org.eclipse.jdt.core.prefs
index f42de363afaae68bbd968318f1d331877f5514fc..0c68a61dca867ceb49e79d2402935261ec3e3809 100644
--- a/org.lamport.tla.toolbox.jclouds/.settings/org.eclipse.jdt.core.prefs
+++ b/org.lamport.tla.toolbox.jclouds/.settings/org.eclipse.jdt.core.prefs
@@ -1,7 +1,7 @@
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7
-org.eclipse.jdt.core.compiler.compliance=1.7
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.7
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/org.lamport.tla.toolbox.jclouds/META-INF/MANIFEST.MF b/org.lamport.tla.toolbox.jclouds/META-INF/MANIFEST.MF
index 94db04f77392ef8f82baba987adac31b52249c3e..479158e7d497873bd7e06c5bb47a8aeebb7e9d67 100644
--- a/org.lamport.tla.toolbox.jclouds/META-INF/MANIFEST.MF
+++ b/org.lamport.tla.toolbox.jclouds/META-INF/MANIFEST.MF
@@ -4,7 +4,7 @@ Bundle-Name: JCloud distributed TLC provider
Bundle-SymbolicName: org.lamport.tla.toolbox.jclouds;singleton:=true
Bundle-Version: 1.0.0.qualifier
Bundle-Vendor: Markus Alexander Kuppe
-Bundle-RequiredExecutionEnvironment: JavaSE-1.7
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Require-Bundle: org.eclipse.core.runtime,
jclouds-core;bundle-version="1.7.3",
jclouds-compute;bundle-version="1.7.3",
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
index 85e30988980c22dc64b20157e64e120a62f35a4c..939751b67cadb60c21549cecf87bdf782392707a 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/Application.java
@@ -26,6 +26,9 @@
package org.lamport.tla.toolbox.jcloud;
import java.io.File;
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.IOException;
import java.text.DateFormat;
import java.text.SimpleDateFormat;
import java.util.Date;
@@ -55,7 +58,7 @@ public class Application implements IApplication {
final String[] args = (String[]) argObject;
final String modelDirectory = args[0];
- final Properties props = new Properties();
+ final Properties props = initializeFromFile(modelDirectory);
props.put(TLCJobFactory.MAIN_CLASS, tlc2.TLC.class.getName());
// Optional parameters
@@ -108,6 +111,11 @@ public class Application implements IApplication {
// Show error message if any such as invalid credentials.
if (status.getSeverity() == IStatus.ERROR) {
System.err.println(status.getMessage());
+ final Throwable exception = status.getException();
+ if (exception instanceof CloudDistributedTLCJob.ScriptException) {
+ System.err.printf("\n###############################\n\n%s\n###############################\n",
+ exception.getMessage());
+ }
// Signal unsuccessful execution.
return new Integer(1);
}
@@ -115,6 +123,15 @@ public class Application implements IApplication {
return IApplication.EXIT_OK;
}
+ private Properties initializeFromFile(final String modelDirectory) throws IOException, FileNotFoundException {
+ final Properties props = new Properties();
+ final File file = new File(modelDirectory + File.separator + "cloud.properties");
+ if (file.exists()) {
+ props.load(new FileInputStream(file));
+ }
+ return props;
+ }
+
/* (non-Javadoc)
* @see org.eclipse.equinox.app.IApplication#stop()
*/
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java
index 5bc266f4cc5b0202d1f6283486303c208ca09ef3..b817c193dc56b61804c68ee705d494a867af85a4 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java
@@ -26,6 +26,8 @@
package org.lamport.tla.toolbox.jcloud;
+import java.io.File;
+
import org.eclipse.core.runtime.Assert;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Status;
@@ -44,20 +46,16 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
*/
@Override
public String getJavaVMArgs() {
- if (numberOfWorkers == 1) {
- return getJavaWorkerVMArgs();
- }
- // See org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob.getAdditionalVMArgs()
- return "--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions -Xmx96G -Xms96G";
+ return System.getProperty("azure.vmargs", super.getJavaVMArgs("-Xmx96G -Xms96G"));
}
-
+
/* (non-Javadoc)
* @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getJavaWorkerVMArgs()
*/
@Override
public String getJavaWorkerVMArgs() {
- // See org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob.getAdditionalVMArgs()
- return "--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions -Xmx32G -Xms32G -XX:MaxDirectMemorySize=64g";
+ return System.getProperty("azure.vmworkerargs",
+ super.getJavaWorkerVMArgs("-Xmx32G -Xms32G -XX:MaxDirectMemorySize=64g"));
}
/* (non-Javadoc)
@@ -65,14 +63,7 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
*/
@Override
public String getTLCParameters() {
- if (numberOfWorkers == 1) {
- if (tlcParams.length() > 0) {
- return "-workers 16 " + tlcParams;
- }
- return "-workers 16";
- } else {
- return "-coverage 0 -checkpoint 0";
- }
+ return System.getProperty("azure.tlcparams", super.getTLCParameters(16));
}
/* (non-Javadoc)
@@ -88,7 +79,7 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
*/
@Override
public String getRegion() {
- return "us-east";
+ return System.getProperty("azure.region", "us-east");
}
/* (non-Javadoc)
@@ -98,7 +89,7 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
public String getImageId() {
// 'azure vm image list eastus canonical' (manually lookup image release date from output)
// With azure-cli v2 (based on Python) extract date from 'az vm image list --all --publisher Canonical'.
- return "b39f27a8b8c64d52b05eac6a62ebad85__Ubuntu-16_04-LTS-amd64-server-20170919-en-us-30GB";
+ return System.getProperty("azure.image", "b39f27a8b8c64d52b05eac6a62ebad85__Ubuntu-16_04-LTS-amd64-server-20180112-en-us-30GB");
}
/* (non-Javadoc)
@@ -106,9 +97,8 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
*/
@Override
public String getHardwareId() {
- return "STANDARD_D14";
- // 16 cores
- // 112GB
+ // STANDARD_D14: 16 cores, 112GB
+ return System.getProperty("azure.instanceType", "STANDARD_D14");
}
/* (non-Javadoc)
@@ -152,6 +142,12 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters
+ "and AZURE_COMPUTE_SUBSCRIPTION) are correctly "
+ "set up and picked up by the Toolbox.");
}
+ // Verify that the identity file exists.
+ final File file = new File(identity);
+ if (!file.exists()) {
+ return new Status(Status.ERROR, "org.lamport.tla.toolbox.jcloud", String.format(
+ "The file %s referenced by the AZURE_COMPUTE_IDENTITY environment variable does not exist.", file));
+ }
return Status.OK_STATUS;
}
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
index b609a25b42cf66297098e41d6b8f4e8830ddbacb..2a23604b20bdd7ebf2040dc38e40a41e332a8271 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
@@ -34,9 +34,11 @@ import static org.jclouds.scriptbuilder.domain.Statements.exec;
import java.io.File;
import java.io.FileOutputStream;
import java.io.IOException;
+import java.io.InputStream;
import java.net.URL;
import java.nio.file.Path;
import java.nio.file.Paths;
+import java.util.Map;
import java.util.NoSuchElementException;
import java.util.Properties;
import java.util.Set;
@@ -52,6 +54,7 @@ import org.jclouds.compute.ComputeServiceContext;
import org.jclouds.compute.RunNodesException;
import org.jclouds.compute.RunScriptOnNodesException;
import org.jclouds.compute.domain.ExecChannel;
+import org.jclouds.compute.domain.ExecResponse;
import org.jclouds.compute.domain.NodeMetadata;
import org.jclouds.compute.domain.TemplateBuilder;
import org.jclouds.compute.options.TemplateOptions;
@@ -187,7 +190,7 @@ public class CloudDistributedTLCJob extends Job {
// either monitor standalone tlc2.TLC or TLCServer.
monitor.subTask("Provisioning TLC environment on all node(s)");
final String email = props.getProperty(TLCJobFactory.MAIL_ADDRESS);
- compute.runScriptOnNodesMatching(
+ Map<? extends NodeMetadata, ExecResponse> execResponse = compute.runScriptOnNodesMatching(
inGroup(groupNameUUID),
// Creating an entry in /etc/alias that makes sure system email sent
// to root ends up at the address given by the user. Note that this
@@ -279,6 +282,7 @@ public class CloudDistributedTLCJob extends Job {
+ "ln -s /mnt/tlc/tlc.jfr /var/www/html/tlc.jfr"),
new TemplateOptions().runAsRoot(true).wrapInInitScript(
false));
+ throwExceptionOnErrorResponse(execResponse, "Provisioning TLC environment on all nodes");
monitor.worked(10);
if (monitor.isCanceled()) {
return Status.CANCEL_STATUS;
@@ -286,11 +290,12 @@ public class CloudDistributedTLCJob extends Job {
// Install all security relevant system packages
monitor.subTask("Installing security relevant system package upgrades (in background)");
- compute.runScriptOnNodesMatching(
+ execResponse = compute.runScriptOnNodesMatching(
inGroup(groupNameUUID),
- exec("/usr/bin/unattended-upgrades"),
+ exec("screen -dm -S security bash -c \"/usr/bin/unattended-upgrades\""),
new TemplateOptions().runAsRoot(true).wrapInInitScript(
- false).blockOnComplete(false).blockUntilRunning(false));
+ true).blockOnComplete(false).blockUntilRunning(false));
+ throwExceptionOnErrorResponse(execResponse, "Installing security relevant system package upgrades");
monitor.worked(5);
final long provision = System.currentTimeMillis();
@@ -381,8 +386,14 @@ public class CloudDistributedTLCJob extends Job {
// the old net.schmizz.sshj and an update to the newer com.hierynomus seems
// awful lot of work.
channel = sshClient.execChannel("cat /mnt/tlc/tlc.jfr");
+ final InputStream output = channel.getOutput();
final String cwd = Paths.get(".").toAbsolutePath().normalize().toString() + File.separator;
- ByteStreams.copy(channel.getOutput(), new FileOutputStream(new File(cwd + "tlc.jfr")));
+ final File jfr = new File(cwd + "tlc.jfr");
+ ByteStreams.copy(output, new FileOutputStream(jfr));
+ if (jfr.length() == 0) {
+ System.err.println("Received empty Java Flight recording. Not creating tlc.jfr file");
+ jfr.delete();
+ }
}
// Finally close the ssh connection.
sshClient.disconnect();
@@ -406,8 +417,9 @@ public class CloudDistributedTLCJob extends Job {
return masterHostname.equals(hostname);
};
};
- compute.runScriptOnNodesMatching(isMaster, exec(tlcMasterCommand), new TemplateOptions().runAsRoot(false)
+ execResponse = compute.runScriptOnNodesMatching(isMaster, exec(tlcMasterCommand), new TemplateOptions().runAsRoot(false)
.wrapInInitScript(true).blockOnComplete(false).blockUntilRunning(false));
+ throwExceptionOnErrorResponse(execResponse, "Starting TLC model checker process on the master node");
monitor.worked(5);
final long tlcStartUp = System.currentTimeMillis();
@@ -417,12 +429,13 @@ public class CloudDistributedTLCJob extends Job {
// (*.tla/*.cfg/...) from the jar file to not share the spec
// with the world.
monitor.subTask("Make TLC code available to all worker node(s)");
- compute.runScriptOnNodesMatching(
+ execResponse = compute.runScriptOnNodesMatching(
isMaster,
exec("cp /tmp/tla2tools.jar /var/www/html/tla2tools.jar && "
+ "zip -d /var/www/html/tla2tools.jar model/*.tla model/*.cfg model/generated.properties"),
new TemplateOptions().runAsRoot(true).wrapInInitScript(
false));
+ throwExceptionOnErrorResponse(execResponse, "Make TLC code available to all worker node");
monitor.worked(10);
if (monitor.isCanceled()) {
return Status.CANCEL_STATUS;
@@ -448,7 +461,7 @@ public class CloudDistributedTLCJob extends Job {
// see master startup for comments
monitor.subTask("Starting TLC workers on the remaining node(s) (in background)");
final String privateHostname = Iterables.getOnlyElement(master.getPrivateAddresses());
- compute.runScriptOnNodesMatching(
+ execResponse = compute.runScriptOnNodesMatching(
onWorkers,
exec("cd /mnt/tlc/ && "
+ "wget http://" + privateHostname + "/tla2tools.jar && "
@@ -477,6 +490,7 @@ public class CloudDistributedTLCJob extends Job {
+ "\""),
new TemplateOptions().runAsRoot(false).wrapInInitScript(
true).blockOnComplete(false).blockUntilRunning(false));
+ throwExceptionOnErrorResponse(execResponse, "Starting TLC workers");
monitor.worked(10);
}
@@ -507,6 +521,13 @@ public class CloudDistributedTLCJob extends Job {
// signal error to caller
return new Status(Status.ERROR, "org.lamport.tla.toolbox.jcloud",
e.getMessage(), e);
+ } catch (ScriptException e) {
+ if (context != null) {
+ destroyNodes(context, groupNameUUID);
+ }
+ // signal error to caller
+ return new Status(Status.ERROR, "org.lamport.tla.toolbox.jcloud",
+ e.getTitle(), e);
} finally {
if (context != null) {
// The user has canceled the Toolbox job, take this as a request
@@ -518,6 +539,16 @@ public class CloudDistributedTLCJob extends Job {
}
}
}
+
+ private void throwExceptionOnErrorResponse(final Map<? extends NodeMetadata, ExecResponse> execResponse, final String step) {
+ execResponse.forEach((node, exec) -> {
+ // If the script above failed on any number of nodes for whatever reason, don't
+ // continue but destroy all nodes.
+ if (exec.getExitStatus() > 0) {
+ throw new ScriptException(node, exec, step);
+ }
+ });
+ }
public void setIsCLI(boolean cli) {
this.isCLI = cli;
@@ -539,6 +570,23 @@ public class CloudDistributedTLCJob extends Job {
}
}
+ @SuppressWarnings("serial")
+ class ScriptException extends RuntimeException {
+
+ private final String title;
+
+ public ScriptException(final NodeMetadata node, final ExecResponse exec, final String step) {
+ super(exec.getOutput());
+ this.title = String.format(
+ "Launching TLC on %s unsuccessful.\nStep '%s' failed on node '%s'.",
+ params.getCloudProvider(), step, node.getName());
+ }
+
+ public String getTitle() {
+ return title;
+ }
+ }
+
class CloudStatus extends Status implements ITLCJobStatus {
private final URL url;
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java
index 7cbba7e80648da18bde2b77319612d5c7b21ba2f..da8f3b5f2c6ea27f3855bd5dad8d11bc900a7f8d 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCInstanceParameters.java
@@ -42,25 +42,30 @@ import tlc2.tool.distributed.fp.TLCWorkerAndFPSet;
public abstract class CloudTLCInstanceParameters {
protected final String tlcParams;
- protected final int numberOfWorkers;
+
+ /**
+ * The number of cloud instances to be used. A value of one means
+ * non-distributed TLC. For values greater than 1, distributed TLC is launched.
+ */
+ protected final int numberOfWorkerNodes;
public CloudTLCInstanceParameters(String tlcParams) {
this(tlcParams, 1);
}
- public CloudTLCInstanceParameters(String tlcParams, int numberOfWorkers) {
+ public CloudTLCInstanceParameters(String tlcParams, int numberOfWorkerNodes) {
this.tlcParams = tlcParams;
- this.numberOfWorkers = numberOfWorkers;
+ this.numberOfWorkerNodes = numberOfWorkerNodes;
}
// system properties
public String getJavaSystemProperties() {
- if (numberOfWorkers == 1) {
+ if (numberOfWorkerNodes == 1) {
return getJavaWorkerSystemProperties();
}
//TODO Make this property be read from the generated.properties file
- return "-Dtlc2.tool.distributed.TLCServer.expectedFPSetCount=" + (numberOfWorkers - 1);
+ return "-Dtlc2.tool.distributed.TLCServer.expectedFPSetCount=" + (numberOfWorkerNodes - 1);
}
public String getJavaWorkerSystemProperties() {
@@ -69,28 +74,33 @@ public abstract class CloudTLCInstanceParameters {
}
// vm args
+ public abstract String getJavaVMArgs();
- public String getJavaVMArgs() {
- if (numberOfWorkers == 1) {
+ protected String getJavaVMArgs(final String extraVMArgs) {
+ if (numberOfWorkerNodes == 1) {
return getJavaWorkerVMArgs();
}
// See org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob.getAdditionalVMArgs()
- return "--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions -Xmx56G -Xms56G";
+ return ("--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions " + extraVMArgs).trim();
}
+
+ public abstract String getJavaWorkerVMArgs();
- public String getJavaWorkerVMArgs() {
+ protected String getJavaWorkerVMArgs(final String extraWorkerVMArgs) {
// See org.lamport.tla.toolbox.tool.tlc.job.TLCProcessJob.getAdditionalVMArgs()
- return "--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions -Xmx24G -Xms24G -XX:MaxDirectMemorySize=32g";
+ return ("--add-modules=java.activation -XX:+IgnoreUnrecognizedVMOptions "
+ + extraWorkerVMArgs).trim();
}
// tlc parameters
+ public abstract String getTLCParameters();
- public String getTLCParameters() {
- if (numberOfWorkers == 1) {
+ protected String getTLCParameters(final int numWorkers) {
+ if (numberOfWorkerNodes == 1) {
if (tlcParams.length() > 0) {
- return "-workers 32 " + tlcParams;
+ return "-workers " + numWorkers + " " + tlcParams;
}
- return "-workers 32";
+ return "-workers " + numWorkers;
} else {
return "-coverage 0 -checkpoint 0";
}
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
index 18713d4585f12967fd7c04a13b7804454c3c4183..70edcc21562e3cc2fd5f3c52a53103942fdc0195 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudTLCJobFactory.java
@@ -37,19 +37,15 @@ public class CloudTLCJobFactory implements TLCJobFactory {
private static final String AZURECOMPUTE = "Azure";
private static final String AWS_EC2 = "aws-ec2";
- private static final String AWS_EC2_VM_PROPERTIES = "aws-ec2-props";
@Override
public Job getTLCJob(String aName, File aModelFolder, int numberOfWorkers, final Properties props, String tlcparams) {
Assert.isNotNull(aName);
Assert.isLegal(numberOfWorkers > 0);
- if (AWS_EC2.equals(aName)) {
+ if (AWS_EC2.equalsIgnoreCase(aName)) {
return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
new EC2CloudTLCInstanceParameters(tlcparams, numberOfWorkers));
- } else if (AWS_EC2_VM_PROPERTIES.equals(aName)) {
- return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
- new EC2PropertyCloudTLCInstanceParameters(tlcparams, numberOfWorkers));
- } else if (AZURECOMPUTE.equals(aName)) {
+ } else if (AZURECOMPUTE.equalsIgnoreCase(aName)) {
return new CloudDistributedTLCJob(aName, aModelFolder, numberOfWorkers, props,
new AzureCloudTLCInstanceParameters(tlcparams, numberOfWorkers));
}
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
index bec45e175813361387a36414fac961808e3b2623..cc0146fd5823f123f0a999b74ff526f671d58afd 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
+++ b/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2CloudTLCInstanceParameters.java
@@ -49,25 +49,6 @@ public class EC2CloudTLCInstanceParameters extends CloudTLCInstanceParameters {
return "aws-ec2";
}
- @Override
- public String getImageId() {
- // Ubuntu 64bit 16.04 Xenial
- // http://cloud-images.ubuntu.com/locator/ec2/
- // See http://aws.amazon.com/amazon-linux-ami/instance-type-matrix/
- // for paravirtual vs. hvm
- return getRegion() + "/ami-2931b953"; // "us-east-1,xenial,amd64,hvm:instance-store"
- }
-
- @Override
- public String getRegion() {
- return "us-east-1";
- }
-
- @Override
- public String getHardwareId() {
- return "c3.8xlarge";
- }
-
@Override
public String getIdentity() {
return System.getenv("AWS_ACCESS_KEY_ID");
@@ -110,11 +91,52 @@ public class EC2CloudTLCInstanceParameters extends CloudTLCInstanceParameters {
properties.setProperty(LocationConstants.PROPERTY_REGIONS, getRegion());
}
+ @Override
+ public String getHostnameSetup() {
+ // Lookup public ipv4 hostname and configure /etc/hosts accordingly. Otherwise,
+ // MailSender uses the internal name which increases likelihood of email being
+ // classified/rejected as spam.
+ return "echo \"$(curl -s http://169.254.169.254/latest/meta-data/local-ipv4) $(curl -s http://169.254.169.254/latest/meta-data/public-hostname)\" >> /etc/hosts && hostname $(curl -s http://169.254.169.254/latest/meta-data/public-hostname)";
+ }
+
+
+ /* (non-Javadoc)
+ * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getImageId()
+ */
+ @Override
+ public String getImageId() {
+ // Ubuntu 64bit 16.04 Xenial
+ // http://cloud-images.ubuntu.com/locator/ec2/
+ // See http://aws.amazon.com/amazon-linux-ami/instance-type-matrix/
+ // for paravirtual vs. hvm (if instance startup fails with funny errors
+ // such as symlinks failing to be created, you accidentally picked paravirtual.
+ // "us-east-1,xenial,amd64,hvm:instance-store"
+ final String imageId = System.getProperty("aws-ec2.image", "ami-51025a2b");
+ return getRegion() + "/" + imageId;
+ }
+
+ /* (non-Javadoc)
+ * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getRegion()
+ */
+ @Override
+ public String getRegion() {
+ return System.getProperty("aws-ec2.region", "us-east-1");
+ }
+
+ @Override
+ public String getHardwareId() {
+ return System.getProperty("aws-ec2.instanceType", "c3.8xlarge");
+ }
+
/* (non-Javadoc)
* @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getOSFilesystemTuning()
*/
@Override
public String getOSFilesystemTuning() {
+ return System.getProperty("aws-ec2.tuning", getOSFilesystemTuningDefault());
+ }
+
+ private String getOSFilesystemTuningDefault() {
// Create a raid0 out of the two instance store
// disks and optimize its fs towards performance
// by sacrificing data durability.
@@ -127,11 +149,27 @@ public class EC2CloudTLCInstanceParameters extends CloudTLCInstanceParameters {
+ "mount /dev/md0 /mnt";
}
+ /* (non-Javadoc)
+ * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getJavaVMArgs()
+ */
@Override
- public String getHostnameSetup() {
- // Lookup public ipv4 hostname and configure /etc/hosts accordingly. Otherwise,
- // MailSender uses the internal name which increases likelihood of email being
- // classified/rejected as spam.
- return "echo \"$(curl -s http://169.254.169.254/latest/meta-data/local-ipv4) $(curl -s http://169.254.169.254/latest/meta-data/public-hostname)\" >> /etc/hosts && hostname $(curl -s http://169.254.169.254/latest/meta-data/public-hostname)";
+ public String getJavaVMArgs() {
+ return System.getProperty("aws-ec2.vmargs", super.getJavaVMArgs("-Xmx56G -Xms56G"));
+ }
+
+ /* (non-Javadoc)
+ * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getTLCParameters()
+ */
+ @Override
+ public String getTLCParameters() {
+ return System.getProperty("aws-ec2.tlcparams", super.getTLCParameters(32));
+ }
+
+ /* (non-Javadoc)
+ * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getJavaWorkerVMArgs()
+ */
+ @Override
+ public String getJavaWorkerVMArgs() {
+ return System.getProperty("aws-ec2.vmworkerargs", super.getJavaWorkerVMArgs("-Xmx24G -Xms24G -XX:MaxDirectMemorySize=32g"));
}
}
diff --git a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
index edf28a51befd047507bfcbac901059a307cb111c..40c02f80a09e1516c34d004ea4c57081c28a988a 100644
--- a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
+++ b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
@@ -1,16 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<?pde version="3.5"?>
-<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.5.5.qualifier" useFeatures="true" includeLaunchers="true">
+<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.5.6.qualifier" useFeatures="true" includeLaunchers="true">
<aboutInfo>
<image path="/org.lamport.tla.toolbox.product.standalone/images/splash_small.png"/>
<text>
TLA+ Toolbox provides a user interface for TLA+ Tools.
-This is Version 1.5.5 of 05 January 2018 and includes:
+This is Version 1.5.6 of 29 January 2018 and includes:
- SANY Version 2.1 of 23 July 2017
- - TLC Version 2.11 of 05 January 2018
+ - TLC Version 2.12 of 29 January 2018
- PlusCal Version 1.8 of 07 December 2015
- TLATeX Version 1.0 of 20 September 2017
@@ -78,18 +78,17 @@ openFile
<plugin id="org.eclipse.equinox.ds" autoStart="true" startLevel="2" />
<plugin id="org.eclipse.equinox.http.jetty" autoStart="true" startLevel="3" />
<plugin id="org.eclipse.equinox.http.registry" autoStart="true" startLevel="3" />
+ <plugin id="org.eclipse.equinox.event" autoStart="true" startLevel="2" />
+ <plugin id="org.eclipse.equinox.simpleconfigurator" autoStart="true" startLevel="1" />
+ <plugin id="org.eclipse.update.configurator"/>
<plugin id="org.lamport.tla.toolbox.jclouds" autoStart="true" startLevel="4" />
<plugin id="sts" autoStart="true" startLevel="4" />
- <property name="eclipse.buildId" value="1.5.5" />
+ <property name="eclipse.buildId" value="1.5.6" />
</configurations>
<repositories>
<repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
<repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
- <repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
- <repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
- <repository location="http://lamport.org/tlatoolbox/toolboxUpdate/" enabled="true" />
- <repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
</repositories>
<preferencesInfo>
diff --git a/org.lamport.tla.toolbox.product.product/pom.xml b/org.lamport.tla.toolbox.product.product/pom.xml
index 6e6620fbc72313c159012f715944da293dd50ec3..677493d61447a7e2b3db34aa550c23aa9205f6fa 100644
--- a/org.lamport.tla.toolbox.product.product/pom.xml
+++ b/org.lamport.tla.toolbox.product.product/pom.xml
@@ -19,7 +19,7 @@
<!-- Align product.version with the version in
org.lamport.tla.toolbox.product.product.product
product.version. -->
- <product.version>1.5.5</product.version>
+ <product.version>1.5.6</product.version>
<!-- Format build timestamp to adhere to the Debian package guidelines -->
<maven.build.timestamp.format>yyyyMMdd-HHmm</maven.build.timestamp.format>
<product.build>${maven.build.timestamp}</product.build>
diff --git a/org.lamport.tla.toolbox.product.standalone/plugin.xml b/org.lamport.tla.toolbox.product.standalone/plugin.xml
index c923097f13130ae81093a68d26fffad6659448e7..279444dede17aa3a097718c329cbc6fafdffc5d7 100644
--- a/org.lamport.tla.toolbox.product.standalone/plugin.xml
+++ b/org.lamport.tla.toolbox.product.standalone/plugin.xml
@@ -30,7 +30,7 @@
</property>
<property
name="aboutText"
- value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.5 of 05 January 2018 and includes:
 - SANY Version 2.1 of 23 July 2017
 - TLC Version 2.11 of 05 January 2018
 - PlusCal Version 1.8 of 07 December 2015
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .">
+ value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.6 of 29 January 2018 and includes:
 - SANY Version 2.1 of 23 July 2017
 - TLC Version 2.12 of 29 January 2018
 - PlusCal Version 1.8 of 07 December 2015
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .">
</property>
<property
name="aboutImage"
diff --git a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
index 1f53e15fd813e0d9f4e409992bae15279ea2e5a8..a0060c28ca84f47f79122fc2c949f514e68e01e2 100644
--- a/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
+++ b/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
@@ -175,7 +175,7 @@ public class ToolboxIntroPart extends IntroPart implements IIntroPart {
final Label lblVersion = new Label(outerContainer, SWT.WRAP);
lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
- lblVersion.setText("Version 1.5.5 of 05 January 2018");
+ lblVersion.setText("Version 1.5.6 of 29 January 2018");
lblVersion.setBackground(backgroundColor);
}
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
index 14b3f28c275e5b84ad2e97e90f57220030d87494..74f9b228047158c1a22e8b36e375302a30f9f03c 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java
@@ -686,7 +686,7 @@ public class ModelEditor extends FormEditor
* @throws CoreException
*/
public void launchModel(final String mode, final boolean userPased, final IProgressMonitor monitor) {
- if (model.isSnapshot()) {
+ if (userPased && model.isSnapshot()) {
final boolean launchSnapshot = MessageDialog.openConfirm(getSite().getShell(), "Model is a snapshot",
"The model which is about to launch is a snapshot of another model. "
+ "Beware that no snapshots of snapshots are taken. "
diff --git a/org.lamport.tla.toolbox.uitest/.classpath b/org.lamport.tla.toolbox.uitest/.classpath
index 64c5e31b7a264082f4c1dfdabb8097de820e66ce..eca7bdba8f03f22510b7980a94dbfe10c16c0901 100644
--- a/org.lamport.tla.toolbox.uitest/.classpath
+++ b/org.lamport.tla.toolbox.uitest/.classpath
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/>
+ <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="bin"/>
diff --git a/org.lamport.tla.toolbox.uitest/.settings/org.eclipse.jdt.core.prefs b/org.lamport.tla.toolbox.uitest/.settings/org.eclipse.jdt.core.prefs
index 30014cb53cea574755555dace687a098fced1066..0c68a61dca867ceb49e79d2402935261ec3e3809 100644
--- a/org.lamport.tla.toolbox.uitest/.settings/org.eclipse.jdt.core.prefs
+++ b/org.lamport.tla.toolbox.uitest/.settings/org.eclipse.jdt.core.prefs
@@ -1,8 +1,7 @@
-#Mon Jun 27 17:02:33 CEST 2011
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
-org.eclipse.jdt.core.compiler.compliance=1.5
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.5
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF b/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
index e02cdafc7fb1deaa64f188e81650d972f4fac051..f29ed17cc4a83105f50378ce332312798c05198e 100644
--- a/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
+++ b/org.lamport.tla.toolbox.uitest/META-INF/MANIFEST.MF
@@ -4,14 +4,14 @@ Bundle-Name: Generic Toolbox Test
Bundle-SymbolicName: org.lamport.tla.toolbox.uitest
Bundle-Version: 1.0.0.qualifier
Bundle-Vendor: Leslie Lamport, Markus Alexander Kuppe
-Bundle-RequiredExecutionEnvironment: J2SE-1.5
+Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Import-Package: org.eclipse.core.resources,
- org.lamport.tla.toolbox.editor.basic,
org.osgi.framework;version="1.3.0"
Require-Bundle: org.eclipse.swt;bundle-version="3.5.0";visibility:=reexport,
org.eclipse.swtbot.go;bundle-version="2.0.0";visibility:=reexport,
org.aspectj.runtime;bundle-version="1.6.0";visibility:=reexport,
org.lamport.tla.toolbox;bundle-version="1.0.0";visibility:=reexport,
+ org.lamport.tla.toolbox.editor.basic;bundle-version="1.0.0",
org.apache.log4j;visibility:=reexport,
org.eclipse.ui.editors;bundle-version="3.9.0",
org.eclipse.ui.forms;bundle-version="3.6.200"
diff --git a/tlatools/src/pcal/ParseAlgorithm.java b/tlatools/src/pcal/ParseAlgorithm.java
index 7b878cbbe3f104c0cab3864d2f05ab75696624d6..faa9f19c9caf00333bd27ee752ba8632bda51d7b 100644
--- a/tlatools/src/pcal/ParseAlgorithm.java
+++ b/tlatools/src/pcal/ParseAlgorithm.java
@@ -1384,9 +1384,13 @@ public class ParseAlgorithm
{ result.Do = new Vector() ;
result.Do.addElement(InnerGetWith(depth+1, begLoc)) ;
};
- result.setOrigin(new Region(begLoc,
- ((AST) result.Do.elementAt(result.Do.size()-1)).getOrigin().getEnd())) ;
- return result ;
+ try {
+ result.setOrigin(new Region(begLoc,
+ ((AST) result.Do.elementAt(result.Do.size()-1)).getOrigin().getEnd())) ;
+ } catch (ArrayIndexOutOfBoundsException e) {
+ throw new ParseAlgorithmException("Missing body of with statement", result);
+ }
+ return result ;
}
public static AST.Assign GetAssign() throws ParseAlgorithmException
diff --git a/tlatools/src/tla2sany/modanalyzer/ParseUnit.java b/tlatools/src/tla2sany/modanalyzer/ParseUnit.java
index 994692db3d331d98bbd6915ec5d87e04c79d9b36..1e5f83216ea7556ef3875b5d08a8bae561de03f7 100644
--- a/tlatools/src/tla2sany/modanalyzer/ParseUnit.java
+++ b/tlatools/src/tla2sany/modanalyzer/ParseUnit.java
@@ -24,6 +24,7 @@ package tla2sany.modanalyzer;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
+import java.nio.file.Path;
import tla2sany.semantic.AbortException;
import tla2sany.semantic.Errors;
@@ -234,6 +235,16 @@ public class ParseUnit {
}
// Print user feedback
+ // MAK 01/2018: Always print the absolute path. Useful if e.g. users symlink
+ // common TLA files and want to verify that symlinking worked.
+ Path absoluteResolvedPath;
+ try {
+ absoluteResolvedPath = nis.getAbsoluteResolvedPath();
+ } catch (IOException e1) {
+ // Fall back to to relative path if resolving the path to an absolute one fails.
+ // Chance of failure should be fairly low because existence is checked above.
+ absoluteResolvedPath = nis.sourceFile().toPath();
+ }
/***********************************************************************
* This is a bug. The higher-level parsing methods have a PrintStream *
* argument to which such output gets written. That argument should *
@@ -244,10 +255,10 @@ public class ParseUnit {
***********************************************************************/
if (ToolIO.getMode() == ToolIO.SYSTEM)
{
- ToolIO.out.println("Parsing file " + nis.sourceFile());
+ ToolIO.out.printf("Parsing file %s\n", absoluteResolvedPath);
} else
{
- ToolIO.out.println("Parsing module " + nis.getModuleName() + " in file " + nis.sourceFile());
+ ToolIO.out.printf("Parsing module %s in file %s\n", nis.getModuleName(), absoluteResolvedPath);
}
boolean parseSuccess;
diff --git a/tlatools/src/tla2sany/semantic/LevelNode.java b/tlatools/src/tla2sany/semantic/LevelNode.java
index eb8ab78bb2b43b45e17c6f8e81373c1b117ea783..002613d603cdbcf23bfa2197068b24602db9d877 100644
--- a/tlatools/src/tla2sany/semantic/LevelNode.java
+++ b/tlatools/src/tla2sany/semantic/LevelNode.java
@@ -192,6 +192,10 @@ public int levelChecked = 0 ;
/***************************************************************************
* The checks in the following methods should probably be eliminated after *
* SANY2 is debugged. *
+* <ul><li>0 for constant *
+* <li>1 for non-primed variable *
+* <li>2 for primed variable *
+* <li>3 for temporal formula</ul> *
***************************************************************************/
public int getLevel(){
if (this.levelChecked == 0)
diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index 0780ec0f071f42b04b6ddf212faeff200e474416..0e646f6abd2b07c9402d29afb1a5fd21a27a62ef 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -22,7 +22,7 @@ public class TLCGlobals
{
// The current version of TLC
- public static String versionOfTLC = "Version 2.11 of 05 January 2018";
+ public static String versionOfTLC = "Version 2.12 of 29 January 2018";
// The bound for set enumeration, used for pretty printing
public static int enumBound = 2000;
diff --git a/tlatools/src/tlc2/tool/ActionItemList.java b/tlatools/src/tlc2/tool/ActionItemList.java
index 2a1cfe8f53ecca727ea14ca73deac08e4b39ce78..236a9dea92ebd138bfec2585e7dc95cb60524126 100644
--- a/tlatools/src/tlc2/tool/ActionItemList.java
+++ b/tlatools/src/tlc2/tool/ActionItemList.java
@@ -7,17 +7,29 @@ import tla2sany.semantic.SemanticNode;
import tlc2.util.Context;
public class ActionItemList {
+ /**
+ * predicate of a conjunction
+ */
+ public static final int CONJUNCT = 0;
+ /**
+ * predicate
+ */
+ public static final int PRED = -1;
+ /**
+ * UNCHANGED predicate
+ */
+ public static final int UNCHANGED = -2;
+ /**
+ * pred' # pred
+ */
+ public static final int CHANGED = -3;
+
/**
* We assume that this.pred is null iff the list is empty.
- * The meaning of this.kind is given as follows:
- * kind > 0: pred of a conjunction
- * kind = -1: pred
- * kind = -2: UNCHANGED pred
- * kind = -3: pred' # pred
*/
public final SemanticNode pred; // Expression of the action
public final Context con; // Context of the action
- public final int kind;
+ private final int kind;
public final ActionItemList next;
public final static ActionItemList
@@ -36,6 +48,13 @@ public class ActionItemList {
public final Context carContext() { return this.con; }
+ /**
+ * The meaning of this.kind is given as follows:
+ * kind > 0: pred of a conjunction
+ * kind = -1: pred
+ * kind = -2: UNCHANGED pred
+ * kind = -3: pred' # pred
+ */
public final int carKind() { return this.kind; }
public final ActionItemList cdr() { return this.next; }
diff --git a/tlatools/src/tlc2/tool/EvalControl.java b/tlatools/src/tlc2/tool/EvalControl.java
index 4c110b0ddd3425831ba15f164ad00174260cb0c2..0626219697c97133187adaf154de66c288ba6f0f 100644
--- a/tlatools/src/tlc2/tool/EvalControl.java
+++ b/tlatools/src/tlc2/tool/EvalControl.java
@@ -8,13 +8,34 @@ package tlc2.tool;
public class EvalControl {
public static final int KeepLazy = 1;
- public static final int Primed = 2;
- public static final int Enabled = 4;
-
+ /**
+ * Current evaluation within a primed variable. If isPrimed is true, lookup in
+ * the Context chain terminates on a branch.
+ *
+ * @see tlc2.util.Context.lookup(SymbolNode, boolean)
+ */
+ public static final int Primed = 1 << 1;
+ /**
+ * Current evaluation scope is within ENABLED. In the ENABLED scope, caching of
+ * LazyValue is disabled.
+ */
+ public static final int Enabled = 1 << 2;
+ /**
+ * Evaluation in the scope of {@link Tool#getInitStates()} or
+ * {@link Tool#getInitStates(IStateFunctor)}. In other words set during the
+ * generation of initial states.
+ */
+ public static final int Init = 1 << 3;
+
public static final int Clear = 0;
+ private static boolean isSet(final int control, final int constant) {
+ // Zero all bits except constant bit(s).
+ return (control & constant) > 0;
+ }
+
public static boolean isKeepLazy(int control) {
- return (control & KeepLazy) > 0;
+ return isSet(control, KeepLazy);
}
public static int setKeepLazy(int control) {
@@ -22,15 +43,32 @@ public class EvalControl {
}
public static boolean isPrimed(int control) {
- return (control & Primed) > 0;
+ return isSet(control, Primed);
}
public static int setPrimed(int control) {
return control | Primed;
}
+ /**
+ * Sets {@link EvalControl#Primed} iff {@link EvalControl#Enabled} is already set.
+ */
+ public static int setPrimedIfEnabled(int control) {
+ if (isEnabled(control)) {
+ return setPrimed(control);
+ }
+ return control;
+ }
+
public static boolean isEnabled(int control) {
- return (control & Enabled) > 0;
+ return isSet(control, Enabled);
+ }
+
+ public static int setEnabled(int control) {
+ return control | Enabled;
}
+ public static boolean isInit(int control) {
+ return isSet(control, Init);
+ }
}
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 81bed024e392ba7acf726b38e29d5c56c2520e61..c671f792da93291e9356568b199d82a235e31645 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -1747,16 +1747,11 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
return opNode;
}
- public final Object getVal(ExprOrOpArgNode expr, Context c, boolean cachable)
+ public final Object getVal(ExprOrOpArgNode expr, Context c, final boolean cachable)
{
if (expr instanceof ExprNode)
{
- LazyValue lval = new LazyValue(expr, c);
- if (!cachable)
- {
- lval.setUncachable();
- }
- return lval;
+ return new LazyValue(expr, c, cachable);
}
SymbolNode opNode = ((OpArgNode) expr).getOp();
return this.lookup(opNode, c, false);
diff --git a/tlatools/src/tlc2/tool/Tool.java b/tlatools/src/tlc2/tool/Tool.java
index ad239434093d26e76378a92a5c58a158f4223cb1..f31392c0162c0f3129b042291d65d07c35f6cc3c 100644
--- a/tlatools/src/tlc2/tool/Tool.java
+++ b/tlatools/src/tlc2/tool/Tool.java
@@ -13,6 +13,8 @@ import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.LabelNode;
import tla2sany.semantic.LetInNode;
+import tla2sany.semantic.LevelConstants;
+import tla2sany.semantic.LevelNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpArgNode;
@@ -310,23 +312,23 @@ public class Tool
* probably make tools like TLC useless.
*/
public final StateVec getInitStates() {
- final StateVec initStates = new StateVec(0);
- getInitStates(initStates);
- return initStates;
+ final StateVec initStates = new StateVec(0);
+ getInitStates(initStates);
+ return initStates;
}
public final void getInitStates(IStateFunctor functor) {
- Vect init = this.getInitStateSpec();
- ActionItemList acts = ActionItemList.Empty;
- for (int i = 1; i < init.size(); i++) {
- Action elem = (Action)init.elementAt(i);
- acts = acts.cons(elem.pred, elem.con, -1);
- }
- if (init.size() != 0) {
- Action elem = (Action)init.elementAt(0);
- TLCState ps = TLCState.Empty.createEmpty();
- this.getInitStates(elem.pred, acts, elem.con, ps, functor);
- }
+ Vect init = this.getInitStateSpec();
+ ActionItemList acts = ActionItemList.Empty;
+ for (int i = 1; i < init.size(); i++) {
+ Action elem = (Action)init.elementAt(i);
+ acts = acts.cons(elem.pred, elem.con, ActionItemList.PRED);
+ }
+ if (init.size() != 0) {
+ Action elem = (Action)init.elementAt(0);
+ TLCState ps = TLCState.Empty.createEmpty();
+ this.getInitStates(elem.pred, acts, elem.con, ps, functor);
+ }
}
/* Create the state specified by pred. */
@@ -463,17 +465,17 @@ public class Tool
if (val instanceof LazyValue) {
LazyValue lv = (LazyValue)val;
- if (lv.val == null || lv.val == ValUndef) {
+ if (lv.getValue() == null || lv.isUncachable()) {
this.getInitStates(lv.expr, acts, lv.con, ps, states);
return;
}
- val = lv.val;
+ val = lv.getValue();
}
Object bval = val;
if (alen == 0) {
if (val instanceof MethodValue) {
- bval = ((MethodValue)val).apply(EmptyArgs, EvalControl.Clear);
+ bval = ((MethodValue)val).apply(EmptyArgs, EvalControl.Init);
}
}
else {
@@ -482,52 +484,10 @@ public class Tool
Value[] argVals = new Value[alen];
// evaluate the actuals:
for (int i = 0; i < alen; i++) {
- /*
- * MAK 12/2017: Effectively disable LazyValues by passing null to this.eval(..).
- * This has the same effect as calling LazyValue#setUncachable upon the creation
- * of a LV. However, at this stack level, the LV has long been created. It can
- * not be set to be uncachable anymore. This changes fixes Github issue 113:
- * "TLC fails to find initial states with bounded exists"
- * https://github.com/tlaplus/tlaplus/issues/113. The corresponding unit test is
- * tlc2.tool.AssignmentInitTest.
- *
- * The bug to fix is, that a the use of an LV breaks evaluation of expressions
- * such as:
- *
- * Op(var) == var \in {0,1} /\ var > 0
- *
- * Op2(var) == \E val \in {0,1} : var = val /\ var > 0
- *
- * The "var" is represented by an instance of a LazyValue which only gets
- * evaluated once. In the two examples above, the LV statically evaluates to "0"
- * even when it should evaluate to "1".
- *
- * If the init predicate is defined to such that:
- *
- * VARIABLE s Init == Op2(s) ...
- *
- * TLC won't generate the initial state s=1. Likewise, the following expression
- * causes TLC to generate two initial states (s=0 and s=1). Again, because the
- * predicate "var < 1" is both times evaluated with "var=0".
- *
- * Init(var) == \E val \in 0..1: var = val /\ var < 1
- *
- * Unfortunately, this disables LazyValues for _all_ operators. It affects all
- * operators such as IF THEN ELSE, Print, ... Disabling LV only for affected
- * operators appears impossible at this stack level. We would somehow have to
- * pass along the call context. Alternatively, an attempt could be made to call
- * LazyValue#setUncachable upon creation of the LV. However, the LV gets created
- * before the call stack "sees" the actual operator.
- *
- * If similar expressions are evaluated in the context of the next-state
- * relation, line ~921 is responsible. It boils down to line 2059 (opcode prime)
- * to disable LV by passing null to tlc2.tool.Tool.evalAppl(...) effectively
- * disabling LVs.
- */
- argVals[i] = this.eval(args[i], c, ps, null, EvalControl.Clear);
+ argVals[i] = this.eval(args[i], c, ps, TLCState.Empty, EvalControl.Init);
}
// apply the operator:
- bval = opVal.apply(argVals, EvalControl.Clear);
+ bval = opVal.apply(argVals, EvalControl.Init);
}
}
@@ -567,7 +527,7 @@ public class Tool
case OPCODE_be: // BoundedExists
{
SemanticNode body = args[0];
- ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Clear);
+ ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init);
Context c1;
while ((c1 = Enum.nextElement()) != null) {
this.getInitStates(body, acts, c1, ps, states);
@@ -577,7 +537,7 @@ public class Tool
case OPCODE_bf: // BoundedForall
{
SemanticNode body = args[0];
- ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Clear);
+ ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init);
Context c1 = Enum.nextElement();
if (c1 == null) {
this.getInitStates(acts, ps, states);
@@ -586,7 +546,7 @@ public class Tool
ActionItemList acts1 = acts;
Context c2;
while ((c2 = Enum.nextElement()) != null) {
- acts1 = acts1.cons(body, c2, -1);
+ acts1 = acts1.cons(body, c2, ActionItemList.PRED);
}
this.getInitStates(body, acts1, c1, ps, states);
}
@@ -594,7 +554,7 @@ public class Tool
}
case OPCODE_ite: // IfThenElse
{
- Value guard = this.eval(args[0], c, ps);
+ Value guard = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init);
if (!(guard instanceof BoolValue)) {
Assert.fail("In computing initial states, a non-boolean expression (" +
guard.getKindString() + ") was used as the condition " +
@@ -614,7 +574,7 @@ public class Tool
other = pairArgs[1];
}
else {
- Value bval = this.eval(pairArgs[0], c, ps);
+ Value bval = this.eval(pairArgs[0], c, ps, TLCState.Empty, EvalControl.Init);
if (!(bval instanceof BoolValue)) {
Assert.fail("In computing initial states, a non-boolean expression (" +
bval.getKindString() + ") was used as a guard condition" +
@@ -635,11 +595,11 @@ public class Tool
}
case OPCODE_fa: // FcnApply
{
- Value fval = this.eval(args[0], c, ps);
+ Value fval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init);
if (fval instanceof FcnLambdaValue) {
FcnLambdaValue fcn = (FcnLambdaValue)fval;
if (fcn.fcnRcd == null) {
- Context c1 = this.getFcnContext(fcn, args, c, ps, TLCState.Empty, EvalControl.Clear);
+ Context c1 = this.getFcnContext(fcn, args, c, ps, TLCState.Empty, EvalControl.Init);
this.getInitStates(fcn.body, acts, c1, ps, states);
return;
}
@@ -650,8 +610,8 @@ public class Tool
fval.getKindString() + ") was applied as a function.\n" + init);
}
Applicable fcn = (Applicable) fval;
- Value argVal = this.eval(args[1], c, ps);
- Value bval = fcn.apply(argVal, EvalControl.Clear);
+ Value argVal = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init);
+ Value bval = fcn.apply(argVal, EvalControl.Init);
if (!(bval instanceof BoolValue))
{
Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "initial states", "boolean",
@@ -666,7 +626,7 @@ public class Tool
{
SymbolNode var = this.getVar(args[0], c, false);
if (var == null || var.getName().getVarLoc() < 0) {
- Value bval = this.eval(init, c, ps);
+ Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init);
if (!((BoolValue)bval).val) {
return;
}
@@ -674,7 +634,7 @@ public class Tool
else {
UniqueString varName = var.getName();
Value lval = ps.lookup(varName);
- Value rval = this.eval(args[1], c, ps);
+ Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init);
if (lval == null) {
ps = ps.bind(varName, rval, init);
this.getInitStates(acts, ps, states);
@@ -694,7 +654,7 @@ public class Tool
{
SymbolNode var = this.getVar(args[0], c, false);
if (var == null || var.getName().getVarLoc() < 0) {
- Value bval = this.eval(init, c, ps);
+ Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init);
if (!((BoolValue)bval).val) {
return;
}
@@ -702,7 +662,7 @@ public class Tool
else {
UniqueString varName = var.getName();
Value lval = ps.lookup(varName);
- Value rval = this.eval(args[1], c, ps);
+ Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init);
if (lval == null) {
if (!(rval instanceof Enumerable)) {
Assert.fail("In computing initial states, the right side of \\IN" +
@@ -728,7 +688,7 @@ public class Tool
}
case OPCODE_implies:
{
- Value lval = this.eval(args[0], c, ps);
+ Value lval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init);
if (!(lval instanceof BoolValue)) {
Assert.fail("In computing initial states of a predicate of form" +
" P => Q, P was " + lval.getKindString() + "\n." + init);
@@ -750,7 +710,7 @@ public class Tool
default:
{
// For all the other builtin operators, simply evaluate:
- Value bval = this.eval(init, c, ps);
+ Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init);
if (!(bval instanceof BoolValue)) {
Assert.fail("In computing initial states, TLC expected a boolean expression," +
@@ -915,10 +875,10 @@ public class Tool
if (val instanceof LazyValue) {
LazyValue lv = (LazyValue)val;
- if (lv.val == null || lv.val == ValUndef) {
+ if (lv.getValue() == null || lv.isUncachable()) {
return this.getNextStates(lv.expr, acts, lv.con, s0, s1, nss);
}
- val = lv.val;
+ val = lv.getValue();
}
Object bval = val;
@@ -996,7 +956,7 @@ public class Tool
ActionItemList acts1 = acts;
Context c2;
while ((c2 = Enum.nextElement()) != null) {
- acts1 = acts1.cons(body, c2, -1);
+ acts1 = acts1.cons(body, c2, ActionItemList.PRED);
}
resState = this.getNextStates(body, acts1, c1, s0, s1, nss);
}
@@ -1031,7 +991,7 @@ public class Tool
}
case OPCODE_aa: // AngleAct <A>_e
{
- ActionItemList acts1 = acts.cons(args[1], c, -3);
+ ActionItemList acts1 = acts.cons(args[1], c, ActionItemList.CHANGED);
return this.getNextStates(args[0], acts1, c, s0, s1, nss);
}
case OPCODE_sa: // [A]_e
@@ -1246,7 +1206,7 @@ public class Tool
if (alen != 0) {
ActionItemList acts1 = acts;
for (int i = alen-1; i > 0; i--) {
- acts1 = acts1.cons(args[i], c, -2);
+ acts1 = acts1.cons(args[i], c, ActionItemList.UNCHANGED);
}
return this.processUnchanged(args[0], acts1, c, s0, s1, nss);
}
@@ -1297,7 +1257,7 @@ public class Tool
* current state, and partial next state.
*/
public final Value eval(SemanticNode expr, Context c, TLCState s0,
- TLCState s1, int control) {
+ TLCState s1, final int control) {
if (this.callStack != null) this.callStack.push(expr);
try {
switch (expr.getKind()) {
@@ -1390,8 +1350,8 @@ public class Tool
}
}
- public final Value evalAppl(OpApplNode expr, Context c, TLCState s0,
- TLCState s1, int control) {
+ private final Value evalAppl(OpApplNode expr, Context c, TLCState s0,
+ TLCState s1, final int control) {
if (this.callStack != null) this.callStack.push(expr);
try {
ExprOrOpArgNode[] args = expr.getArgs();
@@ -1406,20 +1366,111 @@ public class Tool
// First, unlazy if it is a lazy value. We cannot use the cached
// value when s1 == null or isEnabled(control).
- if (val instanceof LazyValue) {
- LazyValue lv = (LazyValue)val;
- if (s1 == null ||
- lv.val == ValUndef ||
- EvalControl.isEnabled(control)) {
- val = this.eval(lv.expr, lv.con, s0, s1, control);
- }
- else {
- if (lv.val == null) {
- lv.val = this.eval(lv.expr, lv.con, s0, s1, control);
- }
- val = lv.val;
- }
- }
+ if (val instanceof LazyValue) {
+ final LazyValue lv = (LazyValue) val;
+ if (s1 == null) {
+ val = this.eval(lv.expr, lv.con, s0, null, control);
+ } else if (lv.isUncachable() || EvalControl.isEnabled(control)) {
+ // Never use cached LazyValues in an ENABLED expression. This is why all
+ // this.enabled* methods pass EvalControl.Enabled (the only exclusion being the
+ // call on line line 2799 which passes EvalControl.Primed). This is why we can
+ // be sure that ENALBED expressions are not affected by the caching bug tracked
+ // in Github issue 113 (see below).
+ val = this.eval(lv.expr, lv.con, s0, s1, control);
+ } else {
+ val = lv.getValue();
+ if (val == null) {
+ final Value res = this.eval(lv.expr, lv.con, s0, s1, control);
+ // This check has been suggested by Yuan Yu on 01/15/2018:
+ //
+ // If init-states are being generated, level has to be <= ConstantLevel for
+ // caching/LazyValue to be allowed. If next-states are being generated, level
+ // has to be <= VariableLevel. The level indicates if the expression to be
+ // evaluated contains only constants, constants & variables, constants &
+ // variables and primed variables (thus action) or is a temporal formula.
+ //
+ // This restriction is in place to fix Github issue 113
+ // (https://github.com/tlaplus/tlaplus/issues/113) -
+ // TLC can generate invalid sets of init or next-states caused by broken
+ // LazyValue evaluation. The related tests are AssignmentInit* and
+ // AssignmentNext*. Without this fix TLC essentially reuses a stale lv.val when
+ // it needs to re-evaluate res because the actual operands to eval changed.
+ // Below is Leslie's formal description of the bug:
+ //
+ // The possible initial values of some variable var are specified by a subformula
+ //
+ // F(..., var, ...)
+ //
+ // in the initial predicate, for some operator F such that expanding the
+ // definition of F results in a formula containing more than one occurrence of
+ // var , not all occurring in separate disjuncts of that formula.
+ //
+ // The possible next values of some variable var are specified by a subformula
+ //
+ // F(..., var', ...)
+ //
+ // in the next-state relation, for some operator F such that expanding the
+ // definition of F results in a formula containing more than one occurrence of
+ // var' , not all occurring in separate disjuncts of that formula.
+ //
+ // An example of the first case is an initial predicate Init defined as follows:
+ //
+ // VARIABLES x, ...
+ // F(var) == \/ var \in 0..99 /\ var % 2 = 0
+ // \/ var = -1
+ // Init == /\ F(x)
+ // /\ ...
+ //
+ // The error would not appear if F were defined by:
+ //
+ // F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}
+ // \/ var = -1
+ //
+ // or if the definition of F(x) were expanded in Init :
+ //
+ // Init == /\ \/ x \in 0..99 /\ x % 2 = 0
+ // \/ x = -1
+ // /\ ...
+ //
+ // A similar example holds for case 2 with the same operator F and the
+ // next-state formula
+ //
+ // Next == /\ F(x')
+ // /\ ...
+ //
+ // The workaround is to rewrite the initial predicate or next-state relation so
+ // it is not in the form that can cause the bug. The simplest way to do that is
+ // to expand (in-line) the definition of F in the definition of the initial
+ // predicate or next-state relation.
+ //
+ // Note that EvalControl.Init is only set in the scope of this.getInitStates*,
+ // but not in the scope of methods such as this.isInModel, this.isGoodState...
+ // which are invoked by DFIDChecker and ModelChecker#doInit and doNext. These
+ // invocation however don't pose a problem with regards to issue 113 because
+ // they don't generate the set of initial or next states but get passed fully
+ // generated/final states.
+ //
+ // !EvalControl.isInit(control) means Tool is either processing the spec in
+ // this.process* as part of initialization or that next-states are being
+ // generated. The latter case has to restrict usage of cached LazyValue as
+ // discussed above.
+ final int level = ((LevelNode) lv.expr).getLevel(); // cast to LevelNode is safe because LV only subclass of SN.
+ if ((EvalControl.isInit(control) && level <= LevelConstants.ConstantLevel)
+ || (!EvalControl.isInit(control) && level <= LevelConstants.VariableLevel)) {
+ // The performance benefits of caching values is generally debatable. The time
+ // it takes TLC to check a reasonable sized model of the PaxosCommit [1] spec is
+ // ~2h with, with limited caching due to the fix for issue 113 or without
+ // caching. There is no measurable performance difference even though the change
+ // for issue 113 reduces the cache hits from ~13 billion to ~4 billion. This was
+ // measured with an instrumented version of TLC.
+ // [1] general/performance/PaxosCommit/
+ lv.setValue(res);
+ }
+ val = res;
+ }
+ }
+
+ }
Value res = null;
if (val instanceof OpDefNode) {
@@ -2067,20 +2118,12 @@ public class Tool
}
case OPCODE_prime:
{
- if (EvalControl.isEnabled(control)) {
- // We are now in primed and enabled.
- return this.eval(args[0], c, s1, null, EvalControl.setPrimed(control));
- }
- return this.eval(args[0], c, s1, null, control);
+ return this.eval(args[0], c, s1, null, EvalControl.setPrimedIfEnabled(control));
}
case OPCODE_unchanged:
{
Value v0 = this.eval(args[0], c, s0, TLCState.Empty, control);
- if (EvalControl.isEnabled(control)) {
- // We are now in primed and enabled.
- control = EvalControl.setPrimed(control);
- }
- Value v1 = this.eval(args[0], c, s1, null, control);
+ Value v1 = this.eval(args[0], c, s1, null, EvalControl.setPrimedIfEnabled(control));
return (v0.equals(v1)) ? ValTrue : ValFalse;
}
case OPCODE_aa: // <A>_e
@@ -2094,11 +2137,7 @@ public class Tool
return ValFalse;
}
Value v0 = this.eval(args[1], c, s0, TLCState.Empty, control);
- if (EvalControl.isEnabled(control)) {
- // We are now in primed and enabled.
- control = EvalControl.setPrimed(control);
- }
- Value v1 = this.eval(args[1], c, s1, null, control);
+ Value v1 = this.eval(args[1], c, s1, null, EvalControl.setPrimedIfEnabled(control));
return v0.equals(v1) ? ValFalse : ValTrue;
}
case OPCODE_sa: // [A]_e
@@ -2112,11 +2151,7 @@ public class Tool
return ValTrue;
}
Value v0 = this.eval(args[1], c, s0, TLCState.Empty, control);
- if (EvalControl.isEnabled(control)) {
- // We are now in primed and enabled.
- control = EvalControl.setPrimed(control);
- }
- Value v1 = this.eval(args[1], c, s1, null, control);
+ Value v1 = this.eval(args[1], c, s1, null, EvalControl.setPrimedIfEnabled(control));
return (v0.equals(v1)) ? ValTrue : ValFalse;
}
case OPCODE_cdot:
@@ -2311,25 +2346,27 @@ public class Tool
private final TLCState enabled(ActionItemList acts, TLCState s0, TLCState s1) {
if (acts.isEmpty()) return s1;
- int kind = acts.carKind();
+ final int kind = acts.carKind();
SemanticNode pred = acts.carPred();
Context c = acts.carContext();
ActionItemList acts1 = acts.cdr();
- if (kind > 0) {
+ if (kind > ActionItemList.CONJUNCT) {
TLCState res = this.enabled(pred, acts1, c, s0, s1);
return res;
}
- else if (kind == -1) {
+ else if (kind == ActionItemList.PRED) {
TLCState res = this.enabled(pred, acts1, c, s0, s1);
return res;
}
- if (kind == -2) {
+ if (kind == ActionItemList.UNCHANGED) {
TLCState res = this.enabledUnchanged(pred, acts1, c, s0, s1);
return res;
}
Value v1 = this.eval(pred, c, s0, TLCState.Empty, EvalControl.Enabled);
- // We are now in ENABLED and primed state.
+ // We are now in ENABLED and primed state. Second TLCState parameter being null
+ // effectively disables LazyValue in evalAppl (same effect as
+ // EvalControl.setPrimed(EvalControl.Enabled)).
Value v2 = this.eval(pred, c, s1, null, EvalControl.Primed);
if (v1.equals(v2)) return null;
@@ -2390,7 +2427,7 @@ public class Tool
{
if (val instanceof MethodValue)
{
- bval = ((MethodValue) val).apply(EmptyArgs, EvalControl.Clear);
+ bval = ((MethodValue) val).apply(EmptyArgs, EvalControl.Clear); // EvalControl.Clear is ignored by MethodValuea#apply
}
} else
{
@@ -2426,7 +2463,7 @@ public class Tool
switch (opcode) {
case OPCODE_aa: // AngleAct <A>_e
{
- ActionItemList acts1 = acts.cons(args[1], c, -3);
+ ActionItemList acts1 = acts.cons(args[1], c, ActionItemList.CHANGED);
return this.enabled(args[0], acts1, c, s0, s1);
}
case OPCODE_be: // BoundedExists
@@ -2456,7 +2493,7 @@ public class Tool
Context c2;
while ((c2 = Enum.nextElement()) != null)
{
- acts1 = acts1.cons(body, c2, -1);
+ acts1 = acts1.cons(body, c2, ActionItemList.PRED);
}
return this.enabled(body, acts1, c1, s0, s1);
}
@@ -2514,13 +2551,13 @@ public class Tool
}
case OPCODE_fa: // FcnApply
{
- Value fval = this.eval(args[0], c, s0, s1, EvalControl.setKeepLazy(EvalControl.Enabled));
+ Value fval = this.eval(args[0], c, s0, s1, EvalControl.setKeepLazy(EvalControl.Enabled)); // KeepLazy does not interfere with EvalControl.Enabled in this.evalAppl
if (fval instanceof FcnLambdaValue)
{
FcnLambdaValue fcn = (FcnLambdaValue) fval;
if (fcn.fcnRcd == null)
{
- Context c1 = this.getFcnContext(fcn, args, c, s0, s1, EvalControl.Enabled);
+ Context c1 = this.getFcnContext(fcn, args, c, s0, s1, EvalControl.Enabled); // EvalControl.Enabled passed on to nested this.evalAppl
return this.enabled(fcn.body, acts, c1, s0, s1);
}
fval = fcn.fcnRcd;
@@ -2529,7 +2566,7 @@ public class Tool
{
Applicable fcn = (Applicable) fval;
Value argVal = this.eval(args[1], c, s0, s1, EvalControl.Enabled);
- Value bval = fcn.apply(argVal, EvalControl.Enabled);
+ Value bval = fcn.apply(argVal, EvalControl.Enabled); // EvalControl.Enabled not taken into account by any subclass of Applicable
if (!(bval instanceof BoolValue))
{
Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "ENABLED", "boolean",
@@ -2756,7 +2793,7 @@ public class Tool
try {
SymbolNode var = this.getVar(expr, c, true);
if (var != null) {
- // a state variable:
+ // a state variable, e.g. UNCHANGED var1
UniqueString varName = var.getName();
Value v0 = this.eval(expr, c, s0, s1, EvalControl.Enabled);
Value v1 = s1.lookup(varName);
@@ -2780,11 +2817,11 @@ public class Tool
int opcode = BuiltInOPs.getOpCode(opName);
if (opcode == OPCODE_tup) {
- // a tuple:
+ // a tuple, e.g. UNCHANGED <<var1, var2>>
if (alen != 0) {
ActionItemList acts1 = acts;
for (int i = 1; i < alen; i++) {
- acts1 = acts1.cons(args[i], c, -2);
+ acts1 = acts1.cons(args[i], c, ActionItemList.UNCHANGED);
}
return this.enabledUnchanged(args[0], acts1, c, s0, s1);
}
@@ -2810,8 +2847,35 @@ public class Tool
}
}
- Value v0 = this.eval(expr, c, s0, TLCState.Empty, EvalControl.Enabled);
- Value v1 = this.eval(expr, c, s1, TLCState.Empty, EvalControl.Primed);
+ final Value v0 = this.eval(expr, c, s0, TLCState.Empty, EvalControl.Enabled);
+ // We are in ENABLED and primed but why pass only primed? This appears to
+ // be the only place where we call eval from the ENABLED scope without
+ // additionally passing EvalControl.Enabled. Not passing Enabled allows a
+ // cached LazyValue could be used (see comments above on line 1384).
+ //
+ // The current scope is a nested UNCHANGED in an ENABLED and evaluation is set
+ // to primed. However, UNCHANGED e equals e' = e , so anything primed in e
+ // becomes double-primed in ENABLED UNCHANGED e. This makes it illegal TLA+
+ // which is rejected by SANY's level checking. A perfectly valid spec - where
+ // e is not primed - but that also causes this code path to be taken is 23 below:
+ //
+ // -------- MODULE 23 ---------
+ // VARIABLE t
+ // op(var) == var
+ // Next == /\ (ENABLED (UNCHANGED op(t)))
+ // /\ (t'= t)
+ // Spec == (t = 0) /\ [][Next]_t
+ // ============================
+ //
+ // However, spec 23 causes the call to this.eval(...) below to throw an
+ // EvalException either with EvalControl.Primed. The exception's message is
+ // "In evaluation, the identifier t is either undefined or not an operator."
+ // indicating that this code path is buggy.
+ //
+ // If this bug is ever fixed to make TLC accept spec 23, EvalControl.Primed
+ // should likely be rewritten to EvalControl.setPrimed(EvalControl.Enabled)
+ // to disable reusage of LazyValues on line ~1384 above.
+ final Value v1 = this.eval(expr, c, s1, TLCState.Empty, EvalControl.Primed);
if (!v0.equals(v1)) {
return null;
}
@@ -2975,7 +3039,7 @@ public class Tool
public final Context getFcnContext(FcnLambdaValue fcn, ExprOrOpArgNode[] args,
Context c, TLCState s0, TLCState s1,
- int control) {
+ final int control) {
Context fcon = fcn.con;
int plen = fcn.params.length();
FormalParamNode[][] formals = fcn.params.formals;
@@ -3054,7 +3118,7 @@ public class Tool
/* A context enumerator for an operator application. */
public final ContextEnumerator contexts(OpApplNode appl, Context c, TLCState s0,
- TLCState s1, int control) {
+ TLCState s1, final int control) {
FormalParamNode[][] formals = appl.getBdedQuantSymbolLists();
boolean[] isTuples = appl.isBdedQuantATuple();
ExprNode[] domains = appl.getBdedQuantBounds();
diff --git a/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java b/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java
index 04e41bcefc688fdecb03249d29015a163caca372..12b8424d312438c06f715e964654f9992ff71359 100644
--- a/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/OffHeapDiskFPSet.java
@@ -1132,7 +1132,7 @@ public final class OffHeapDiskFPSet extends NonCheckpointableDiskFPSet implement
protected void writeIndex(long[] index, final RandomAccessFile raf, long length) throws IOException {
for (int i = 0; i < index.length; i++) {
- long pos = Math.min(i * NumEntriesPerPage, length);
+ long pos = Math.min(((long) i) * NumEntriesPerPage, length);
raf.seek(pos * LongSize);
final long value = raf.readLong();
index[i] = value;
diff --git a/tlatools/src/tlc2/tool/liveness/LNStateEnabled.java b/tlatools/src/tlc2/tool/liveness/LNStateEnabled.java
index 8f33d7ee6d484324ba23cfd0288c2e3c45f35732..b07b2275427fc737d62115d2f89b1373428726b1 100644
--- a/tlatools/src/tlc2/tool/liveness/LNStateEnabled.java
+++ b/tlatools/src/tlc2/tool/liveness/LNStateEnabled.java
@@ -51,7 +51,7 @@ class LNStateEnabled extends LNState {
TLCState sfun = TLCStateFun.Empty;
Context c1 = Context.branch(getContext());
if (this.subscript != null) {
- acts = acts.cons(this.subscript, c1, -3);
+ acts = acts.cons(this.subscript, c1, ActionItemList.CHANGED);
}
sfun = tool.enabled(this.pred, acts, c1, s1, sfun);
return sfun != null;
diff --git a/tlatools/src/tlc2/value/LazyValue.java b/tlatools/src/tlc2/value/LazyValue.java
index bb378a6d629003219d9c3e20f746a4a6f3cf14ce..8fe604d9606693dfec1b9816413b9f18e04f9a90 100644
--- a/tlatools/src/tlc2/value/LazyValue.java
+++ b/tlatools/src/tlc2/value/LazyValue.java
@@ -10,13 +10,30 @@ import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
-import tlc2.tool.ModelChecker;
-import tlc2.tool.FingerprintException;
import tla2sany.semantic.SemanticNode;
+import tlc2.tool.FingerprintException;
import tlc2.util.Context;
import util.Assert;
+import util.ToolIO;
public class LazyValue extends Value {
+ /**
+ * Allow to completely disable LazyValue by passing a VM property/system
+ * property to the Java VM with "-Dtlc2.value.LazyValue.off=true". This is meant
+ * for debug purposes only and can be removed at any time. This is not API.
+ *
+ * This property was added 01/12/2018 by Markus Kuppe in the process of fixing a
+ * bug where TLC generates and incorrect set of states with certain statements.
+ * More details can be found at https://github.com/tlaplus/tlaplus/issues/113.
+ */
+ private static final boolean LAZYEVAL_OFF = Boolean.getBoolean(tlc2.value.LazyValue.class.getName() + ".off");
+
+ static {
+ // Indicate if LazyValue will be disabled in this TLC run.
+ if (LAZYEVAL_OFF) {
+ ToolIO.out.println("LazyValue is disabled.");
+ }
+ }
/**
* The field val is the result of evaluating expr in context con and
* a pair of states. If val is null, then the value has not been
@@ -27,16 +44,36 @@ public class LazyValue extends Value {
public SemanticNode expr;
public Context con;
- public Value val;
+ private Value val;
public LazyValue(SemanticNode expr, Context con) {
+ this(expr, con, true);
+ }
+
+ public LazyValue(SemanticNode expr, Context con, final boolean cachable) {
this.expr = expr;
this.con = con;
this.val = null;
+ // See comment on cachable's meager performance in Tool.java on line 1408.
+ // See other note about a bug that surfaced with LazyValue in Tool.java on line ~1385.
+ if (LAZYEVAL_OFF || !cachable) {
+ this.val = ValUndef;
+ }
}
- public final void setUncachable() { this.val = ValUndef; }
+ public final boolean isUncachable() { return this.val == ValUndef; }
+
+ public final void setValue(final Value aValue) {
+ assert !isUncachable();
+ this.val = aValue;
+ }
+ public final Value getValue() {
+ // cache hit on (this.val != null && !isUncachable)
+ // cache miss on (this.val == null)
+ return this.val;
+ }
+
public final byte getKind() { return LAZYVALUE; }
public final int compareTo(Object obj) {
diff --git a/tlatools/src/util/NamedInputStream.java b/tlatools/src/util/NamedInputStream.java
index e635475b00a543ad329bacfe8a621bcdccaae0e7..273dcd4dd0f7c6c248bce436c5a11d427d92dde0 100644
--- a/tlatools/src/util/NamedInputStream.java
+++ b/tlatools/src/util/NamedInputStream.java
@@ -6,6 +6,7 @@ import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
+import java.nio.file.Path;
// SZ Feb 20, 2009: moved to util and reformatted
@@ -65,6 +66,15 @@ public class NamedInputStream extends FileInputStream
{
return inputFile;
}
+
+ /**
+ * @return The absolute, resolved path. In case a file is symlinked, resolve the
+ * final target (doesn't work for cygwin symlinks but for mklink)
+ * @throws IOException
+ */
+ public final Path getAbsoluteResolvedPath() throws IOException {
+ return inputFile.toPath().toRealPath();
+ }
public final String toString()
{
diff --git a/tlatools/test-concurrent/tlc2/tool/fp/MultiThreadedFPSetTest.java b/tlatools/test-concurrent/tlc2/tool/fp/MultiThreadedFPSetTest.java
index d607913bc11d39b46f4c81255b29761e5011d0c4..2959b88da91ea032e54c32b346187a2a32459125 100644
--- a/tlatools/test-concurrent/tlc2/tool/fp/MultiThreadedFPSetTest.java
+++ b/tlatools/test-concurrent/tlc2/tool/fp/MultiThreadedFPSetTest.java
@@ -104,6 +104,7 @@ public abstract class MultiThreadedFPSetTest extends AbstractFPSetTest {
TLCGlobals.setNumWorkers(NUM_THREADS);
final FPSet fpSet = getFPSetInitialized(NUM_THREADS);
+ fpSet.incWorkers(NUM_THREADS);
final CountDownLatch latch = new CountDownLatch(NUM_THREADS);
final Constructor<?> constructor = fpgClass.getConstructor(new Class[] { MultiThreadedFPSetTest.class,
diff --git a/tlatools/test-model/AssignmentInit.tla b/tlatools/test-model/AssignmentInit.tla
index e8919f6eb8854a86274513e433499dab2638dbe7..54c495e3c4a08c9665a035e5cc9b769c5bceced5 100644
--- a/tlatools/test-model/AssignmentInit.tla
+++ b/tlatools/test-model/AssignmentInit.tla
@@ -1,5 +1,5 @@
--------------------------- MODULE AssignmentInit ---------------------------
-EXTENDS Integers
+EXTENDS Integers, TLC
VARIABLE s
min(S) == CHOOSE e \in S: \A a \in S: e <= a
@@ -10,6 +10,11 @@ InitAll(var, S) == \A val \in S: (var = val /\ var \in S)
InitIn(var, S) == var \in S /\ var > min(S)
+InitEq(var, S, val) == var \in S /\ var + 1 = val
+
+isOdd(n) == n % 2 = 1
+InitEven(var, S) == var \in S /\ isOdd(var)
+
\* With this Init(var), the test does not fail without its fix.
\*Init(ignored) == \E val \in {0,1}: (s = val /\ s > 0)
@@ -18,6 +23,8 @@ Spec == /\ \/ InitExit(s, {0,1}) \* 1 unique state
\/ InitAll(s, {2}) \* 1 unique state
\/ InitIn(s, {4,5}) \* 1 unique state
\/ InitAll(s, {6,7}) \* 0 unique states
- /\ [][UNCHANGED s]_s
+ \/ InitEq(s, {8,9}, 10) \* 1 unique states
+ \/ InitEven(s, {10,11}) \* 1 unique states
+ /\ [][InitExit(s, {0,1})/\UNCHANGED s]_s
=============================================================================
diff --git a/tlatools/test-model/AssignmentNext2.cfg b/tlatools/test-model/AssignmentNext2.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..bc224b9def594b0819de3f0b45ede63ea8213c7b
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext2.cfg
@@ -0,0 +1,2 @@
+SPECIFICATION
+Spec
diff --git a/tlatools/test-model/AssignmentNext2.tla b/tlatools/test-model/AssignmentNext2.tla
new file mode 100644
index 0000000000000000000000000000000000000000..fa337732111cdd97afea05adc986bdfb5ebdfd63
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext2.tla
@@ -0,0 +1,9 @@
+--------------------------- MODULE AssignmentNext2 ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+Next(var) == \E val \in 0..1: (var = val /\ var > 0)
+
+Spec == s = "" /\ [][Next(s')]_s
+
+=============================================================================
diff --git a/tlatools/test-model/AssignmentNext3.cfg b/tlatools/test-model/AssignmentNext3.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..bc224b9def594b0819de3f0b45ede63ea8213c7b
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext3.cfg
@@ -0,0 +1,2 @@
+SPECIFICATION
+Spec
diff --git a/tlatools/test-model/AssignmentNext3.tla b/tlatools/test-model/AssignmentNext3.tla
new file mode 100644
index 0000000000000000000000000000000000000000..9843f1a755efb077eb20961bbd4b304583d2bef8
--- /dev/null
+++ b/tlatools/test-model/AssignmentNext3.tla
@@ -0,0 +1,9 @@
+--------------------------- MODULE AssignmentNext3 ---------------------------
+EXTENDS Integers
+VARIABLE s
+
+F(var) == (var \in 0..9 /\ (var % 2 = 0))
+
+Spec == s=0 /\ [][F(s')]_s
+
+=============================================================================
diff --git a/tlatools/test-model/MissingBodyInWith.tla b/tlatools/test-model/MissingBodyInWith.tla
new file mode 100644
index 0000000000000000000000000000000000000000..e674a3270aac01eb55c69c8975e79d4118509f8a
--- /dev/null
+++ b/tlatools/test-model/MissingBodyInWith.tla
@@ -0,0 +1,10 @@
+------------------------------ MODULE MissingBodyInWith ------------------------------
+(***************************************************************************
+--algorithm MissingBodyInWith
+begin
+ with x = 0 do
+ end with;
+end algorithm
+ ***************************************************************************)
+
+=============================================================================
diff --git a/tlatools/test/pcal/MissingBodyInWithTest.java b/tlatools/test/pcal/MissingBodyInWithTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..5df279e7a4a54820ce2ca6d828943ed426d74eb6
--- /dev/null
+++ b/tlatools/test/pcal/MissingBodyInWithTest.java
@@ -0,0 +1,30 @@
+package pcal;
+
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertNull;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.tool.CommonTestCase;
+import util.ToolIO;
+
+public class MissingBodyInWithTest {
+
+ @Test
+ public void test() {
+ // Make tool capture the output written to ToolIO.out. Otherwise,
+ // ToolIO#getAllMessages returns an empty array.
+ ToolIO.setMode(ToolIO.TOOL);
+
+ assertNull(trans.runMe(new String[] {"-nocfg", CommonTestCase.BASE_PATH + "MissingBodyInWith.tla"}));
+
+ final String[] messages = ToolIO.getAllMessages();
+ assertTrue(messages.length == 1);
+
+ final String msg = messages[0];
+ assertEquals("Unrecoverable error:\n" +
+ " -- Missing body of with statement\n" +
+ " at line 5, column 5.", msg.trim());
+ }
+}
diff --git a/tlatools/test/tlc2/tool/AssignmentInitTest.java b/tlatools/test/tlc2/tool/AssignmentInitTest.java
index b6d75e72740aec382347fd4b124477eb342b4b60..78fe339dae1621f5495f5b3b2bd012d462f2dbfa 100644
--- a/tlatools/test/tlc2/tool/AssignmentInitTest.java
+++ b/tlatools/test/tlc2/tool/AssignmentInitTest.java
@@ -43,6 +43,6 @@ public class AssignmentInitTest extends ModelCheckerTestCase {
public void test() {
assertTrue(recorder.recorded(EC.TLC_FINISHED));
assertFalse(recorder.recorded(EC.GENERAL));
- assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "6", "3", "0"));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "6", "5", "0"));
}
}
diff --git a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java b/tlatools/test/tlc2/tool/AssignmentNext2Test.java
similarity index 56%
rename from org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java
rename to tlatools/test/tlc2/tool/AssignmentNext2Test.java
index ab82f89ca01e666defb162293c50cf28ed8e87a3..b92c86bd844e421bd131e8e833f39f7327dc18f3 100644
--- a/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/EC2PropertyCloudTLCInstanceParameters.java
+++ b/tlatools/test/tlc2/tool/AssignmentNext2Test.java
@@ -23,45 +23,26 @@
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
-package org.lamport.tla.toolbox.jcloud;
+package tlc2.tool;
-public class EC2PropertyCloudTLCInstanceParameters extends EC2CloudTLCInstanceParameters {
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
- public EC2PropertyCloudTLCInstanceParameters(final String tlcParams, int numberOfWorkers) {
- super(tlcParams.trim(), numberOfWorkers);
- }
-
- @Override
- public String getImageId() {
- final String imageId = System.getProperty("aws-ec2.image");
- if (imageId == null) {
- return super.getImageId();
- }
- return getRegion() + "/" + imageId;
- }
+import org.junit.Test;
- @Override
- public String getRegion() {
- return System.getProperty("aws-ec2.region", super.getRegion());
- }
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
- @Override
- public String getHardwareId() {
- return System.getProperty("aws-ec2.instanceType", super.getHardwareId());
- }
-
- @Override
- public String getOSFilesystemTuning() {
- return System.getProperty("aws-ec2.tuning", super.getOSFilesystemTuning());
- }
+public class AssignmentNext2Test extends ModelCheckerTestCase {
- @Override
- public String getJavaVMArgs() {
- return System.getProperty("aws-ec2.vmargs", super.getJavaVMArgs());
+ public AssignmentNext2Test() {
+ super("AssignmentNext2");
}
- @Override
- public String getTLCParameters() {
- return System.getProperty("aws-ec2.tlcparams", super.getTLCParameters());
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "3", "2", "0"));
}
}
diff --git a/tlatools/test/tlc2/tool/AssignmentNext3Test.java b/tlatools/test/tlc2/tool/AssignmentNext3Test.java
new file mode 100644
index 0000000000000000000000000000000000000000..8831dafa87ad0ce33c6b2c8e1c3abf88d339263f
--- /dev/null
+++ b/tlatools/test/tlc2/tool/AssignmentNext3Test.java
@@ -0,0 +1,48 @@
+/*******************************************************************************
+ * Copyright (c) 2017 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ * Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool;
+
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class AssignmentNext3Test extends ModelCheckerTestCase {
+
+ public AssignmentNext3Test() {
+ super("AssignmentNext3");
+ }
+
+ @Test
+ public void test() {
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertFalse(recorder.recorded(EC.GENERAL));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "26", "5", "0"));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/EvalControlTest.java b/tlatools/test/tlc2/tool/EvalControlTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..7e869cf8691a3a42aa00248b8b28abd9a9b4ba93
--- /dev/null
+++ b/tlatools/test/tlc2/tool/EvalControlTest.java
@@ -0,0 +1,43 @@
+package tlc2.tool;
+
+import static org.junit.Assert.*;
+
+import org.junit.Test;
+
+public class EvalControlTest {
+
+ @Test
+ public void test() {
+ int control = EvalControl.Clear;
+
+ assertFalse(EvalControl.isEnabled(control));
+ assertFalse(EvalControl.isKeepLazy(control));
+ assertFalse(EvalControl.isPrimed(control));
+
+ control = EvalControl.setEnabled(control);
+ assertTrue(EvalControl.isEnabled(control));
+ assertFalse(EvalControl.isKeepLazy(control));
+ assertFalse(EvalControl.isPrimed(control));
+
+ control = EvalControl.setKeepLazy(control);
+ assertTrue(EvalControl.isEnabled(control));
+ assertTrue(EvalControl.isKeepLazy(control));
+ assertFalse(EvalControl.isPrimed(control));
+
+ control = EvalControl.setPrimed(control);
+ assertTrue(EvalControl.isEnabled(control));
+ assertTrue(EvalControl.isKeepLazy(control));
+ assertTrue(EvalControl.isPrimed(control));
+ }
+
+ @Test
+ public void testIfEnabled() {
+ int control = EvalControl.Clear;
+
+ assertFalse(EvalControl.isPrimed(EvalControl.setPrimedIfEnabled(control)));
+
+ control = EvalControl.setEnabled(control);
+ assertTrue(EvalControl.isEnabled(control));
+ assertTrue(EvalControl.isPrimed(EvalControl.setPrimedIfEnabled(control)));
+ }
+}
diff --git a/tlatools/test/tlc2/tool/fp/OffHeapDiskFPSetTest.java b/tlatools/test/tlc2/tool/fp/OffHeapDiskFPSetTest.java
index be6422e9817e6ad9647f108bc83132f6262e9322..3980851c00b6fc2fde73661eed700e38dddba699 100644
--- a/tlatools/test/tlc2/tool/fp/OffHeapDiskFPSetTest.java
+++ b/tlatools/test/tlc2/tool/fp/OffHeapDiskFPSetTest.java
@@ -28,10 +28,12 @@ package tlc2.tool.fp;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertTrue;
+import static org.junit.Assert.fail;
import static tlc2.tool.fp.DiskFPSet.MARK_FLUSHED;
import static tlc2.tool.fp.OffHeapDiskFPSet.EMPTY;
import java.io.File;
+import java.io.FileNotFoundException;
import java.io.IOException;
import java.lang.reflect.Field;
import java.lang.reflect.InvocationTargetException;
@@ -289,4 +291,40 @@ public class OffHeapDiskFPSetTest {
final long fp = (((long) random.nextInt(Integer.MAX_VALUE - 1) + 1) << 32) | (random.nextInt() & 0xffffffffL);
return fp;
}
+
+ @Test
+ public void testWriteIndex() throws NoSuchFieldException, SecurityException, IllegalArgumentException,
+ IllegalAccessException, NoSuchMethodException, InvocationTargetException, IOException {
+ final DummyFPSetConfiguration fpSetConfig = new DummyFPSetConfiguration();
+ fpSetConfig.setMemoryInFingerprintCnt(1);
+
+ final OffHeapDiskFPSet fpSet = new OffHeapDiskFPSet(fpSetConfig);
+ final Method method = OffHeapDiskFPSet.class.getDeclaredMethod("writeIndex",
+ new Class[] { long[].class, java.io.RandomAccessFile.class, long.class });
+ method.setAccessible(true);
+
+ // length of array times NumEntriesPerPage has to exceed Integer.MAX_VALUE
+ final int length = 99999999;
+ assertTrue(length * DiskFPSet.NumEntriesPerPage < 1);
+
+ try {
+ method.invoke(fpSet, new long[length], new DummyRandomAccessFile(File.createTempFile("foo", "bar"), "rw"),
+ Integer.MAX_VALUE);
+ } catch (InvocationTargetException e) {
+ Throwable targetException = e.getTargetException();
+ fail(targetException.getMessage());
+ }
+ }
+
+ private static class DummyRandomAccessFile extends java.io.RandomAccessFile {
+
+ public DummyRandomAccessFile(File file, String mode) throws FileNotFoundException {
+ super(file, mode);
+ }
+
+ @Override
+ public int read() throws IOException {
+ return 0;
+ }
+ }
}