TLA+ | The way to specify » Recent Topics

TLA+ | The way to specify » Recent Topics http://bbpress.tlaplus.net/ The TLA+ and PlusCal Resource en-US Wed, 22 Feb 2012 23:41:58 +0000 http://bbpress.org/?v=1.0.2 <![CDATA[Search]]> q http://bbpress.tlaplus.net/search.php CharpoV on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-165 Tue, 07 Feb 2012 20:48:32 +0000 CharpoV 165@http://bbpress.tlaplus.net/ This old bug is getting to be really annoying, especially now that it shows up even in the simplest examples I use in a class I'm teaching on TLA/TLC (and severely undermines my message on the beauty of model-checking). Is there a version of TLC in which the bug has been fixed (I'm using the command-line tools, not the fancy toolbox)? Will it ever be fixed? How is it that I seem to be the only user who gets into this problem with astounding regularity? Below is a small module that exhibits the problem. The trace produced by TLC is clearly not a valid counterexample to the leads-to. MC Module: <code> -------------------- MODULE X -------------------- EXTENDS Naturals VARIABLES x, b A == /\ x < 5 /\ b /\ b' = ~b /\ UNCHANGED x B == /\ ~b /\ b' = ~b /\ x' = x + 1 Init == x \in 0..3 /\ b \in BOOLEAN Prog == Init /\ [][A \/ B]_<<x, b>> /\ WF_<<x, b>>(A \/ B) -------------------------------------------------------------------------------- Xshrinks == x=2 ~> x=1 ================================================================================ </code> Trace: <code> State 1: <Initial predicate> /\ b = FALSE /\ x = 3 State 2: <Action line 13, col 3 to line 15, col 15 of module X> /\ b = TRUE /\ x = 4 State 3: <Action line 7, col 3 to line 10, col 16 of module X> /\ b = FALSE /\ x = 4 State 4: <Action line 13, col 3 to line 15, col 15 of module X> /\ b = TRUE /\ x = 5 State 5: Stuttering </code> groban on "Hi - Newbee Question" http://bbpress.tlaplus.net/topic/hi-newbee-question#post-149 Sun, 10 Jul 2011 10:10:31 +0000 groban 149@http://bbpress.tlaplus.net/ I am trying to understand both TLA+ and toolbox. I am useing toolbox-64 on windows 7 prof 64bit. I am testing the hourclock example. ok. I am changing HCnxt with the following 'HCnxt == IF hr' # 14 THEN hr+1 ELSE 1' This change shouldn't make my theorem incorrect? I am running model checker and it founds no errors. Also in the model checker when i am clicking in the header of the column an empty new window with no state graph is presented. Finally, when i am trying to lanch model prover (with right click) it creates an error message that doesn't find c:/cygwin/bin. Does the toolbox needs cygwin pre-installed? Thanks for your time CharpoV on "(old) leads-to bug" http://bbpress.tlaplus.net/topic/old-leads-to-bug#post-161 Thu, 17 Nov 2011 23:56:04 +0000 CharpoV 161@http://bbpress.tlaplus.net/ I'm seing (again) a counterexample for a property of the form p ~> q in which the cycle of states is such that p is always false. This is a longstanding bug (I can provide the module if needed). In my desperation, I tried to use the toolbox instead of the command-line tools (although it looks both use TLC2 Version 2.03 of 20 July 2011). What I get then is "java.io.EOFException". Also, is setting Java's class path to toolbox/plugins/org.lamport.tlatools_1.0.0.201109181126 equivalent to using the command-line tools? MC CharpoV on "Feature request" http://bbpress.tlaplus.net/topic/feature-request#post-160 Thu, 17 Nov 2011 17:24:50 +0000 CharpoV 160@http://bbpress.tlaplus.net/ TLC won't let me use: \A <<x,y>> \in AllRouters, s \in Sides : LET q == grid[x, y][s].in IN \/ q = <<>> \/ Head(q).header # <<x,y>> However, this ugly alternative works: ... IN IF q = <<>> THEN TRUE ELSE Head(q).header # <<x,y>> Could TLC's evaluation of disjunctions be improved to avoid the problem? Or is there a non-ugly alternative that I'm missing? (Note: I'm using the command-line tools, TLC2 Version 2.03 of 20 July 2011.) MC sid_rao on ""Successor state is not completely specified by the next-state action" error" http://bbpress.tlaplus.net/topic/successor-state-is-not-completely-specified-by-the-next-state-action-error#post-158 Mon, 24 Oct 2011 17:10:35 +0000 sid_rao 158@http://bbpress.tlaplus.net/ Hi, I have some experience with TLA+. Currently, I am writing a specification which gives the following error, "Error: Successor state is not completely specified by the next-state action." The transition function in the model which causes this error is, BootRomOp == /\ pc = "rom" /\ BootRom_state' = IF (BootRom_corrupt=0) THEN "malicious" ELSE "good" /\ pc' = "boot" /\ UNCHANGED <<variables>> ---end--- However, the error goes away and TLC completes successfully, if I remove the "IF THEN ELSE" construct from the above transition function, and reformulate the function as, for example, BootRomOp == /\ pc = "rom" /\ BootRom_state' = "good" /\ pc' = "boot" /\ UNCHANGED <<variables>> ----end----- Can someone give me an insight into why I am getting the "Successor state is not completely specified" error? Parul on "TLA+ Specification" http://bbpress.tlaplus.net/topic/tla-specification#post-156 Sun, 25 Sep 2011 19:51:07 +0000 Parul 156@http://bbpress.tlaplus.net/ Hi, I am new to TLA.I am exploring TLA+ tools and i am facing problems in this.I have following queries 1)I want to know how to get output for any code.suppose we write code for factorial program(in which we are calculating factorial of a number) so where we will get its output. 2)How to check a model with tlc when there is no liveness property? Thanks in advance Leslie Lamport on "Introduction to the Distributed TLC Forum" http://bbpress.tlaplus.net/topic/introduction-to-the-distributed-tlc-forum#post-155 Thu, 15 Sep 2011 11:39:01 +0000 Leslie Lamport 155@http://bbpress.tlaplus.net/ The next release of the TLA+ Toolbox will allow TLC to run in distributed mode. You will be able to execute a TLC run in parallel on dozens or hundreds of computers, potentially speeding up model checking by one or two orders of magnitude. However, this will require automating the process of starting the workers, and we don't know how to do that on all the different operating systems and networks that people use. The purpose of this forum is for users to share their experiences of running TLC in distributed mode, so we can all learn what works on what kinds of systems. kbanks on "Creating a Sequence from a Set?" http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set#post-123 Sun, 12 Dec 2010 09:16:34 +0000 kbanks 123@http://bbpress.tlaplus.net/ If I have a set like a = {1,2,3} and I create a Sequence b = Sequence(a), I get a sequence of length 1, with the sole element being the set. In other words, b = <<{1,2,3}>>. What is the right way to somehow enumerate over the set, so I can define a set of things in my config (.cfg) file, and make a sequence from them in my .tla file? (My intent was to wind up with b = <<1,2,3>>) mkoconnor on "Nullpointerexception" http://bbpress.tlaplus.net/topic/nullpointerexception#post-150 Fri, 19 Aug 2011 09:18:18 +0000 mkoconnor 150@http://bbpress.tlaplus.net/ First of all, thanks for this! It looks great. I get a Null Pointer exception every time I try to run TLC on any model (i.e., click the Green run model button). I'm not sure what all information you need, but I'm on a Mac and this is the toolbox version: This is Version 1.3.1 of 5 April 2011 and includes: - SANY Version 2.1 of 10 February 2011 - TLC Version 2.03 of 26 May 2010 - PlusCal Version 1.5 of 19 March 2011 - TLATeX Version .9 of 19 September 2007 and this is my machine and Java versions: $ uname -a Darwin Michael-OConnors-MacBook-Pro.local 10.8.0 Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386 i386 $ java -version java version "1.6.0_26" Java(TM) SE Runtime Environment (build 1.6.0_26-b03-384-10M3425) Java HotSpot(TM) 64-Bit Server VM (build 20.1-b02-384, mixed mode) Thanks! Leslie Lamport on "Coming Soon: Parallel Execution of TLC on a Network" http://bbpress.tlaplus.net/topic/coming-soon-parallel-execution-of-tlc-on-a-network#post-148 Tue, 28 Jun 2011 10:39:24 +0000 Leslie Lamport 148@http://bbpress.tlaplus.net/ We are going to enhance the Toolbox and the TLC model checker to enable running TLC on a network of machines. We hope this will provide a speedup that is linear in the number of machines for dozens and perhaps hundreds of machines. Because of the variety of networks that people might use, we cannot make it as easy to use TLC on a network as on a single machine. To try to make it reasonably easy for must users, we would like to find out how this will be used. If you would be likely to use this feature, please let us know how you would use it. You can either post to this forum or send email to Leslie Lamport (<a href="http://lamport.org">http://lamport.org</a>) briefly describing: <ul> <li> What operating system(s) you will be using.</li> <li> The network of computers you will be using, including its bandwidth, the number of machines and the kinds of machines (how many cores and how much memory they have).</li> <li> How the computer running the Toolbox will be connected to the network running TLC, and if it will be continuously connected to the network throughout a TLC run. </li> <li> If possible, the approximate number of distinct states generated by the models you would like to check.</li> </ul> When run on a network, TLC will check only safety properties, not liveness properties. (The liveness-checking algorithm cannot easily be parallelized.) cnewcom on "Best way to define transitive closure as an operator for TLC?" http://bbpress.tlaplus.net/topic/best-way-to-define-transitive-closure-as-an-operator-for-tlc#post-141 Sun, 05 Jun 2011 23:05:38 +0000 cnewcom 141@http://bbpress.tlaplus.net/ Does anyone have a definition of a transitive closure operator that is efficient for TLC to evaluate? A paper [1] shows that transitive closure cannot be defined in first order logic, but it can be defined in Datalog, as datalog guarantees to use the least-fixed-point solution. I would use this CHOOSE solution, which appears to work for small test cases. But per [2], TLA+ does not guarantee that CHOOSE finds the least fix-point solution, which means this definition is incorrect (I think). This definition is also very slow in TLC, for anything other than tiny inputs. IsTransitive(r) == \A x, y, z \in Univ : <<x, y>> \in r /\ <<y, z>> \in r => <<x, z>> \in r TCChoose(r) == CHOOSE TCr \in SUBSET (Univ \X Univ) : /\ r \subseteq TCr (* \subset doesn't parse, why? p273 *) /\ IsTransitive(TCr) /\ (* No smaller value meets the same conditions *) ~ \E tuple \in TCr : LET one_smaller == TCr \ {tuple} IN /\ r \subseteq one_smaller /\ IsTransitive(one_smaller) I wrote a constructive version that recurs until reaching least fixpoint (below). But I’m planning to make heavy use of this operator, so I’d like to know if there’s a faster way. Also, I recall reading that it’s possible to implement particular TLA+ modules in Java, for TLC. Has anyone found that to be worth the effort? Thanks, Chris TCRecur(r) == LET RECURSIVE selfJoin(_) selfJoin(r1) == LET MissingJoinTuples(left,right) == {<<x, z>> \in (Univ \X Univ) : /\ <<x, z>> \notin left /\ <<x, z>> \notin right /\ \E y \in Univ : <<x, y>> \in left /\ <<y, z>> \in right} mjt == MissingJoinTuples(r1, r1) IN IF mjt = {} THEN r1 (* have reached least fixpoint, so this must be transitive closure *) ELSE LET bigger == r1 \union mjt IN bigger \union selfJoin(bigger) IN selfJoin(r) (* Test constant expressions, with Univ <- {a, b, c, d, e, f} TCChoose({<<a, b>>, <<b, c>>, <<d, e>>, <<d, f>>}) = {<<a, b>>, <<a, c>>, <<b, c>>, <<d, e>>, <<d, f>>} *) [1] <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.127.8266&rep=rep1&type=pdf" rel="nofollow">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.127.8266&rep=rep1&type=pdf</a> [2] From <a href="http://www.loria.fr/~merz/papers/tla+logic2008.pdf" rel="nofollow">http://www.loria.fr/~merz/papers/tla+logic2008.pdf</a> Recursive functions can be defined in terms of choice, e.g. factorial _= choose f : f = [n ∈ Nat 7→ if n = 0 then 1 else n ∗ f [n − 1]] which TLA+, using some syntactic sugar, offers to write more concisely as factorial [n ∈ Nat ] _= if n = 0 then 1 else n ∗ factorial [n − 1] Of course, as with any construction based on choice, such a definition should be justified by proving the existence of a function that satisfies the recursive equation. Unlike standard semantics of programming languages, TLA+ does not commit to the least fixed point of a recursively defined function in cases where there are several solutions. ajholanda on "Spec: Experiment using PID Controller" http://bbpress.tlaplus.net/topic/spec-experiment-using-pid-controller#post-146 Tue, 21 Jun 2011 18:41:19 +0000 ajholanda 146@http://bbpress.tlaplus.net/ Dear All; I am specifying a program to control an physical experiment using TLA+. I think I have my first draft, but of course there is a large room to improvements. I've tried to split the chunks of the specification it is not reliable, but the result appeared very cryptic. So I'm posting the documentation link that contains the specification: <a href="http://dcm.ffclrp.usp.br/~aholanda/pidcon/pidcon.pdf" rel="nofollow">http://dcm.ffclrp.usp.br/~aholanda/pidcon/pidcon.pdf</a> Some doubts: 1. At page 8 the function "DoPerodicMeasures" is specified, but now that I am studying temporal formulas, it seems to me that I can use them to specify this function. But a doubt occurred to me, when I specify using temporal formulas, some instructions necessary to the implementation are "coupled" into the formulas, it maybe is good in the specification, but the implementation loose a guide. 2. I think I put a lot of implementation details, mainly in the "CondutivityExperiment" specification. 3. I have doubts if "DeviceInterface" is being a good abstraction for the devices. I have to apologize the draft state of the material, but I need some feedback to advance. Any help are welcome. Thanks in advance; Regards; Adriano. giuliano on "Possible bug in TLC?" http://bbpress.tlaplus.net/topic/possible-bug-in-tlc#post-138 Tue, 12 Apr 2011 15:07:34 +0000 giuliano 138@http://bbpress.tlaplus.net/ Hello, I'm having trouble running TLC. I'm using the latest version of the tla tools without the toolbox (just using a terminal on linux). Here is a simplified version of my setup: - I defined two modules, NoCrash and Library, as follows (in two different files): <pre><code>------------------------ MODULE NoCrash ------------------------ EXTENDS Library CONSTANTS X VARIABLES y ----------------------------------- Init == y = TRUE Z == {h \in MySeqs : \E p \in X : TRUE} Next == Z = TRUE ==============================</code></pre> <pre><code>------------------------------- MODULE Library ------------------------------- CONSTANT MySeqs =====================================</code></pre> In order to use TLC I then defined module MCNoCrash as follows: <pre><code>-------------------- MODULE MCNoCrash -------------------------------- EXTENDS Library CONSTANT X BS == [{1} -> {1}] VARIABLE y I == INSTANCE NoCrash Next == I!Next Init == I!Init ============================</code></pre> And the following configuration file: <pre><code>INIT Init NEXT Next CONSTANTS X = {} MySeqs <- BS</code></pre> When running TLC with the command "java -cp ~/tla/tla/ tlc2/TLC MCNoCrash.tla", I get the following output: - Computing initial states... Finished computing initial states: 1 distinct state generated. Error: In evaluation, the identifier X is either undefined or not an operator. - TLC says the error appeared while evaluating the expression "{h \in MySeqs : \E p \in X : TRUE}" - Although my setup is a bit silly I think I shouldn't get this error. For example if I set BS to the empty set instead of [{1} -> {1}] in module MCNoCrash the error disappears. It also disappears if I replace Z by its definition when defining Next in module NoCrash. Is this a bug or am I doing something wrong? I also get the same error in another situation involving instantiation. - Thanks for reading my message, Giuliano Saleem on "Measuring memory usage" http://bbpress.tlaplus.net/topic/measuring-memory-usage#post-68 Sun, 28 Mar 2010 11:36:00 +0000 Saleem 68@http://bbpress.tlaplus.net/ How can we check memory used after verifying the specification/model/query? In verification results, I can just check. 1) Execution time 2) Diameter 3) States found and so on...but I can not check how much memory is used. Can any one help me in finding answer to this question. robson on "WildFire Challenge and TLA+ ToolBox" http://bbpress.tlaplus.net/topic/wildfire-challenge-and-tla-toolbox#post-134 Tue, 05 Apr 2011 21:31:21 +0000 robson 134@http://bbpress.tlaplus.net/ Hi, I am new to TLA+ and I trying explore WildFire spec in TLA+ ToolBox. But, when I open the WildFire.tla and after create a model, It's is reported 13 errors (Model Overview tab) to "Specify the values of declared constants". Can anyone help-me? What is happening. cnewcom on "Toolbox stuck in strange state after system restart while running TLC" http://bbpress.tlaplus.net/topic/toolbox-stuck-in-strange-state-after-system-restart-while-running-tlc#post-131 Tue, 22 Mar 2011 17:54:49 +0000 cnewcom 131@http://bbpress.tlaplus.net/ I'm using Version 1.2.1 of 29 September 2010 (32-bit) Running on Windoes 7 Enterprise 64-bit, on a 4-proc 4GB ThinkPad laptop. Sequence of events: 1. TLC was checking a model. (I can't remember if it was doing it in the background.) 2. I had to do a system restart to install an update of some unrelated software (Adobe Reader). 3. After the restart I ran the toolbox and found that: - TLC is not running (not surprising, as I haven't restarted it.) - The Model Overview tab says "(model checking is in progress)" - The "How to run" options are all greyed out. The "Checkpoint Id" and "Checkpoint Size" are populated with reasonable values, but they are greyed-out. - The "Model Checking Results" tab says "Current Status: Not running" and "Errors detected: No Errors". The "State space progress" box lists the last few state reports (from before the system restart) Note: I did previously stop this TLC run, and restart from a checkpoint, without any problems. But I didn't do a system-restart that time. thanks, Chris kbanks on "Towers of Hanoi and a question about Invariants" http://bbpress.tlaplus.net/topic/towers-of-hanoi-and-a-question-about-invariants#post-124 Tue, 14 Dec 2010 06:24:16 +0000 kbanks 124@http://bbpress.tlaplus.net/ Created an example for the "Towers of Hanoi" logic puzzle, but ran out of time before I could add any error checking using invariants. Anybody got a good suggestion for what I should have verified in <pre><code>(* TypeInvariant == /\ peg1 ??? /\ peg2 ??? /\ peg3 ??? *)</code></pre> Hanoi.tla <pre><code>------------------------------ MODULE Hanoi --------------------------------- (***************************************************************************) (* "Towers of Hanoi" puzzle solved using TLA+ 12/12/2010-12/13/2010 *) (* Transfer a stack of disks from one peg to another, with the constraint *) (* that a larger disk can never be placed on a smaller disk. A third peg *) (* makes the puzzle possible. *) (***************************************************************************) (***************************************************************************) (* Since we care about the SIZE of the disks we represent them as integers *) (* We will represent each peg as a sequence of those disks, with the Head *) (* of each Sequence representing the TOP of that stack of disks. *) (***************************************************************************) EXTENDS Integers, Sequences CONSTANTS NumberOfDisks VARIABLE peg1, peg2, peg3 ----------------------------------------------------------------------------- \* I never did find a way to specify the initial tuple in the .cfg file... Disks == [i \in 1..NumberOfDisks |-> i] Init == /\ peg1 = Disks /\ peg2 = <<>> /\ peg3 = <<>> (* TypeInvariant == /\ peg1 ??? /\ peg2 ??? /\ peg3 ??? *) (***************************************************************************) (* Helper function, needed because the destination peg might be empty *) (* (You cannot take the Head() of an empty Sequence!) *) (* What we do in the "empty peg" case is return a number bigger than ANY *) (* disk. *) (***************************************************************************) Top(peg) == IF peg = <<>> THEN NumberOfDisks+1 ELSE Head(peg) (***************************************************************************) (* A legal move in Hanoi, genericized in terms of src peg, dest peg, and *) (* the spare peg *) (***************************************************************************) MoveDisk(src, dest, spare) == /\ src # <<>> /\ Head(src) < Top(dest) /\ src' = Tail(src) /\ dest' = SubSeq(src,1,1) \o dest /\ UNCHANGED <<spare>> (***************************************************************************) (* The legal moves in Hanoi, specified in terms of MoveDisk. *) (***************************************************************************) MoveTopDiskFromPeg1ToPeg2 == MoveDisk(peg1, peg2, peg3) MoveTopDiskFromPeg1ToPeg3 == MoveDisk(peg1, peg3, peg2) MoveTopDiskFromPeg2ToPeg1 == MoveDisk(peg2, peg1, peg3) MoveTopDiskFromPeg2ToPeg3 == MoveDisk(peg2, peg3, peg1) MoveTopDiskFromPeg3ToPeg1 == MoveDisk(peg3, peg1, peg2) MoveTopDiskFromPeg3ToPeg2 == MoveDisk(peg3, peg2, peg1) Next == \/ MoveTopDiskFromPeg1ToPeg2 \/ MoveTopDiskFromPeg1ToPeg3 \/ MoveTopDiskFromPeg2ToPeg1 \/ MoveTopDiskFromPeg2ToPeg3 \/ MoveTopDiskFromPeg3ToPeg1 \/ MoveTopDiskFromPeg3ToPeg2 Spec == Init /\ [][Next]_<<peg1, peg2, peg3>> ----------------------------------------------------------------------------- Solved == /\ peg1 = <<>> /\ peg2 = <<>> /\ peg3 = Disks NotSolved == ~Solved =============================================================================</code></pre> Hanoi.cfg <pre><code>CONSTANTS NumberOfDisks = 3 SPECIFICATION Spec \*INVARIANTS TypeInvariant NotSolved INVARIANTS NotSolved</code></pre> notpattison on "Trouble with Channels in PlusCal" http://bbpress.tlaplus.net/topic/trouble-with-channels-in-pluscal#post-125 Thu, 03 Feb 2011 05:10:29 +0000 notpattison 125@http://bbpress.tlaplus.net/ I'm a graduate student learning PlusCal in an Independent Study. I'm using PlusCal to model a concurrent system, and I need to use channels and message queues to model communication between processes. I attempted to reuse the Channel and FIFO modules described in the Specifying Systems book, but I'm having trouble. The model I'm creating requires more than one channel so I tried to use INSTANCE to create multiple instances of the Channel module. I used define { InChan == INSTANCE Channel WITH Data <- PassengerNames, chan <- in }. PlusCal failed to translate, and the translator complains about the comma in the InChan definition (I can give you the exact error message in a second post). I also don't know how to make InChan!Init apart of the Init operation generated by PlusCal. Also, I'm having trouble getting a TypeInvariant operation to work. I've had no luck modeling any part of a system in TLA when using PlusCal. Ultimately, I decided to use PlusCal to implement the channels and message queue, but it was tedious work. Do you have any suggestions for geting TLA modules to work in a PlusCal model? kbanks on "By a newbie for fellow newbies - Missionaries and Cannibals" http://bbpress.tlaplus.net/topic/by-a-newbie-for-fellow-newbies-missionaries-and-cannibals#post-122 Sun, 12 Dec 2010 04:36:23 +0000 kbanks 122@http://bbpress.tlaplus.net/ (second attempt at this post - failed the captcha the first time (?)) Fellow beginners may find this example useful. I took what I learned from the "DieHard" example and wrote a TLA+ spec to solve the "Missionaries and Cannibals" puzzle. Config file Cannibal.cfg <pre><code>SPECIFICATION Spec INVARIANTS TypeOK NotSolved</code></pre> Spec file Cannibal.tla <pre><code>------------------------------ MODULE Cannibal ----------------------------- (***************************************************************************) (* The Missionaries and Cannibals Problem solved using TLA+ *) (* Everybody starts on the lhs of the river *) (* The goal is to get everybody safely across the river *) (* The boat can only carry 1 or 2 (never none) *) (* If the cannibals ever outnumber the missionaries, they will eat them! *) (* NOTE-there CAN legally be more cannibals than missionaries on the same *) (* side of the river when the number of missionaries = 0 *) (* Worked on this 12/07/2010-12/08/2010 *) (***************************************************************************) EXTENDS Naturals VARIABLES cl, \* The number of cannibals on the lhs of the river. ml, \* The number of missionaries on the lhs of the river. cr, \* The number of cannibals on the rhs of the river. mr, \* The number of missionaries on the rhs of the river. boat \* 0 when boat is on the lhs, 1 when the boat is on the rhs TypeOK == /\ cl \in 0..3 /\ ml \in 0..3 /\ cr \in 0..3 /\ mr \in 0..3 /\ boat \in 0..1 Init == /\ cl = 3 /\ ml = 3 /\ cr = 0 /\ mr = 0 /\ boat = 0 (***************************************************************************) (* Now we define the actions that can happen. There are ten. *) (* Because the boat changes sides each time a crossing is made, only 5 are *) (* possible at any given time. *) (***************************************************************************) BoatLR1C == /\ boat = 0 /\ cl >= 1 /\ \/ mr = 0 \/ mr >= cr+1 /\ boat' = 1 /\ cl' = cl-1 /\ UNCHANGED <<ml>> /\ cr' = cr+1 /\ UNCHANGED <<mr>> BoatLR2C == /\ boat = 0 /\ cl >= 2 /\ \/ mr = 0 \/ mr >= cr+2 /\ boat' = 1 /\ cl' = cl-2 /\ UNCHANGED <<ml>> /\ cr' = cr+2 /\ UNCHANGED <<mr>> BoatLR1M == /\ boat = 0 /\ ml >= 1 /\ \/ ml-1 = 0 \/ ml-1 >= cl /\ mr+1 >= cr /\ boat' = 1 /\ ml' = ml-1 /\ UNCHANGED <<cl>> /\ mr' = mr+1 /\ UNCHANGED <<cr>> BoatLR2M == /\ boat = 0 /\ ml >= 2 /\ \/ ml-2 = 0 \/ ml-2 >= cl /\ mr+2 >= cr /\ boat' = 1 /\ ml' = ml-2 /\ UNCHANGED <<cl>> /\ mr' = mr+2 /\ UNCHANGED <<cr>> BoatLR1C1M == /\ boat = 0 /\ cl >= 1 /\ ml >= 1 /\ \/ ml-1 = 0 \/ ml-1 >= cl-1 /\ mr+1 >= cr+1 /\ boat' = 1 /\ cl' = cl-1 /\ ml' = ml-1 /\ cr' = cr+1 /\ mr' = mr+1 BoatRL1C == /\ boat = 1 /\ cr >= 1 /\ \/ ml = 0 \/ ml >= cl+1 /\ boat' = 0 /\ cr' = cr-1 /\ UNCHANGED <<mr>> /\ cl' = cl+1 /\ UNCHANGED <<ml>> BoatRL2C == /\ boat = 1 /\ cr >= 2 /\ \/ ml = 0 \/ ml >= cl+2 /\ boat' = 0 /\ cr' = cr-2 /\ UNCHANGED <<mr>> /\ cl' = cl+2 /\ UNCHANGED <<ml>> BoatRL1M == /\ boat = 1 /\ mr >= 1 /\ \/ mr-1 = 0 \/ mr-1 >= cr /\ ml+1 >= cl /\ boat' = 0 /\ mr' = mr-1 /\ UNCHANGED <<cr>> /\ ml' = ml+1 /\ UNCHANGED <<cl>> BoatRL2M == /\ boat = 1 /\ mr >= 2 /\ \/ mr-2 = 0 \/ mr-2 >= cr /\ ml+2 >= cl /\ boat' = 0 /\ mr' = mr-2 /\ UNCHANGED <<cr>> /\ ml' = ml+2 /\ UNCHANGED <<cl>> BoatRL1C1M == /\ boat = 1 /\ cr >= 1 /\ mr >= 1 /\ \/ mr-1 = 0 \/ mr-1 >= cr-1 /\ ml+1 >= cl+1 /\ boat' = 0 /\ cr' = cr-1 /\ mr' = mr-1 /\ cl' = cl+1 /\ ml' = ml+1 Next == \/ BoatLR1C \/ BoatLR2C \/ BoatLR1M \/ BoatLR2M \/ BoatLR1C1M \/ BoatRL1C \/ BoatRL2C \/ BoatRL1M \/ BoatRL2M \/ BoatRL1C1M Spec == Init /\ [][Next]_<<cl, ml, cr, mr, boat>> ----------------------------------------------------------------------------- (***************************************************************************) (* The puzzle is solved when all parties are safely across the river, *) (***************************************************************************) Solved == /\ cl = 0 /\ ml = 0 /\ cr = 3 /\ mr = 3 /\ boat = 1 NotSolved == ~Solved (*NotSolved == \/ cl # 0 \/ ml # 0 \/ cr # 3 \/ mr # 3 \/ boat # 1*) =============================================================================</code></pre> Avinash Joshi on "[TLA+ Toolbox] Multiple tla Tabs" http://bbpress.tlaplus.net/topic/tla-toolbox-multiple-tla-tabs#post-121 Fri, 22 Oct 2010 05:46:56 +0000 Avinash Joshi 121@http://bbpress.tlaplus.net/ Hi. I am are using TLA+ Toolbox on my Ubuntu 10.04 (x64). Toolbox works fine without any hitches. But, I have been trying to open multiple tla files in different tabs, but that does not seem to work for some reason. Whenever I try to open a spec file from the Spec Explorer, it opens in the existing tab and a new tab is not created. How do I fix this? merz on ""Save as ..." pitfall" http://bbpress.tlaplus.net/topic/save-as-pitfall#post-117 Sun, 10 Oct 2010 20:48:48 +0000 merz 117@http://bbpress.tlaplus.net/ Suppose I want to create a variant of a spec MySpec that defines a temporal formula Spec. I edit MySpec.tla and save it as MySpec2.tla, via the "Save as ..." dialog. At this moment, only the frame for MySpec2 is displayed in the toolbox. However, the toolbox treats this file as belonging to MySpec. In particular, when I subsequently create a model and run the model checker, it will use the specification Spec of MySpec.tla, not of MySpec2.tla. If I want to create a model for MySpec2, I must go through the "Open Spec" dialog, even though the specification is (the only one) displayed in the editor. It is not clear to me if this is a bug or a feature, but it would be nice if the GUI could give a better feedback of what it considers the current spec. Thanks, Stephan Frederic Line on "Recursivity and arity" http://bbpress.tlaplus.net/topic/recursivity-and-arity#post-118 Sat, 16 Oct 2010 14:10:09 +0000 Frederic Line 118@http://bbpress.tlaplus.net/ If I define RECURSIVE depthFirst(_,_) depthFirst(f,F(_)) == ... I get the error depthFirst has different arity than its recursive declaration. Maybe it's a bug. SomeBdyElse on "TLC friendly state composition" http://bbpress.tlaplus.net/topic/tlc-friendly-state-composition#post-114 Fri, 06 Aug 2010 18:15:35 +0000 SomeBdyElse 114@http://bbpress.tlaplus.net/ Hi all! I am trying to check the conformity of concurrent Java programs to TLA+ specifications by "running" them in a TLA+ formalization of the JVM specification. In this context I wrote two TLA+ formulas: The first one describes the execution of a single Thread in the JVM, while the second one composes multiple threads and would ideally allow them to move at the same time, if monitors etc allow. It is somehow comparable to the ClockArray example in Mr. Lamport's "Specifying Systems", page 139, just that there are also constraints on the combination of thread states, as if it was (for example) forbidden that multiple clocks show the same time in one global state. Additionally the number of threads that the JVM manages is variable. While the single threads "run" fine in TLC I am troubled to find a good way to express the composition, that TLC accepts. Here is a simplified example of the formulas I would like to get TLC compatible. To make it readable I reduced the complexity of the thread module to a simple program counter and left away the global constraints, which I think I would be able to handle. <pre><code>---- MODULE Thread ---- VARIABLE pc LOCAL INSTANCE Integers ---- Init == pc = 0 Next == pc' = pc+1 ==== ---- MODULE TLAJVM ---- VARIABLE pcs Thread(i) == INSTANCE Thread WITH pc <- pcs[i] ---- Init == (* start with one Thread *) /\ DOMAIN(pcs) = {1} (* Thread!Init has to be true for all threads *) /\ \forall i \in DOMAIN(pcs): Thread(i)!Init Next == (* after a regular "Next" step the amount of threads is still the same *) /\ DOMAIN(pcs') = DOMAIN(pcs) (* all threads step *) /\ \forall i \in DOMAIN(pcs): Thread(i)!Next ====</code></pre> Is there a way to formalize this in a way that TLC takes it? The ClockArray example uses the "IsFcnOn" formula defined on page 140 to describe the global state. However, while humans can compute possible next states out of a given state, the IsFcnOn invariable and the action formulas for each single clock just fine, TLC needs pcs' to be defined as either "pcs' = ..." or "pcs' \in ..." as far as I understand. Does anybody have an idea how to rewrite the above formula to this form? I first thought that the TLA+ translations of multiprocess PlusCal algorithms might yield an example, but after reading the "Next" formula on page 63 of "A PlusCal User's Manual" it seems to me that in PlusCal only one processes is allowed to advance per Next step. For now I have resigned myself to use two alternating actions in the TLAJVM. One that chooses non-deterministically which thread gets run next and a second one that advances that thread while all other threads hold still. However, this introduces interleaving where I would prefer true concurrency and has bad effects on the number of states and the complexity of the mappings I draw from the TLAJVM into the original TLA+ specifications of the programs. Here is a (simplified) version of my current solution: <pre><code>---- MODULE TLAJVM ---- VARIABLE pcs VARIABLE threadMovingI VARIABLE pc VARIABLE move ---- Thread == INSTANCE Thread WITH pc <- pc (* just to be explicit here *) Init == /\ Thread!Init (* this determines pc *) /\ pcs = << pc >> /\ threadMovingI = FALSE /\ move = FALSE Prepare == /\ move = FALSE /\ UNCHANGED pcs /\ threadMovingI' \in DOMAIN(pcs) /\ pc' = pcs[threadMovingI'] /\ move' = TRUE Move == /\ move = TRUE /\ Thread!Next (* this determines pc' *) /\ pcs' = [pcs EXCEPT ![threadMovingI] = pc] /\ threadMovingI' = FALSE /\ move' = FALSE Next == Prepare \/ Move TLAJVM == Init /\ [][Next]_<<pcs,threadMovingI,pc,move>> ====</code></pre> I would be glad if anyone can give me hint how to express true concurrency of the thread movements in a way that TLC can compute the next states and check my refinement mappings. Thanks a lot for reading this far and any thoughts on it you might share ;) pdudnik on "wildfire spec design question" http://bbpress.tlaplus.net/topic/wildfire-spec-design-question#post-108 Fri, 21 May 2010 16:07:23 +0000 pdudnik 108@http://bbpress.tlaplus.net/ Hi, I read the wildfire spec and I saw that transient states were modeled with cache versions. I wonder why the designers of the spec chose to use cache versions rather than true transient states for modeling. Does it have to do with TLC limitations, or is it just a simplification? Thank you. Polina pdudnik on "INSTANCE question" http://bbpress.tlaplus.net/topic/instance-question#post-111 Tue, 25 May 2010 17:11:14 +0000 pdudnik 111@http://bbpress.tlaplus.net/ Hi, I have a question about using INSTANCE. From what I understand, tlc2 is able to handle INSTANCE. So, suppose my purpose in using INSTANCE is to hide some variables. Other than that, I would like to keep everything the same. So, I would say: Inner(param) == INSTANCE MyModule Spec == \E param: MyModule(param)!MySpec and in the config file I would say SPECIFICATION Spec So far, my experience has been that tlc2 complains about this setup because it is not finding init predicate. So, I think it is looking for something of the form Init /\ []Next, and not finding it because it is in MyModule. Is there a way to go about this? Thank you. Polina pdudnik on "memBar and comsig" http://bbpress.tlaplus.net/topic/membar-and-comsig#post-107 Fri, 21 May 2010 15:50:59 +0000 pdudnik 107@http://bbpress.tlaplus.net/ Hi, In the wildfire spec, MB request can be retired once it receives comsig's for all the previous requests. Which means that MB can be retired before all operations ahead of it have actually completed. So, for example, from what I understand the following can happen: Processor 2 has block A. Processor 1 has block A in idle state and would like to write it, so it issues a request to the directory. The directory forwards the request to processor 2 and sends a comsig to processor 1. Because comsig and fill messages travel on separate paths, comsig message can arrive before fill message. In that case, could the following scenario lead to inconsistency: P1 to Dir: get block A Dir to P2: inval block A Dir to P1: comsig Dir to P1: fill block A P1 locally: MB P1 locally: update block B P2 to Dir: get block B Dir to P1: forward block B P1 to P2: block B P2 locally: fill block B P2 locally: read block A P2 locally: inval block A (invalidate message finally arrives) So, essentially, the writes to block A and block B should be ordered by MB, but are observed out of order by processor 2 because MB does not wait for all the fills to complete. Thank you. Polina pdudnik on "Is this forum a good place for questions about the wildfire challenge?" http://bbpress.tlaplus.net/topic/is-this-forum-a-good-place-for-questions-about-the-wildfire-challenge#post-104 Tue, 18 May 2010 22:53:35 +0000 pdudnik 104@http://bbpress.tlaplus.net/ Thank you. Polina Simon Zambrovski on "Specifications" http://bbpress.tlaplus.net/topic/specifications#post-22 Mon, 08 Feb 2010 08:41:01 +0000 Simon Zambrovski 22@http://bbpress.tlaplus.net/ This is a forum for users to post their specification examples only. Please provide a name of the specification and post the ASCII version of TLA+/PlusCal specification into the thread. If you have any questions, feel free to post to the General FAQ forum. pdudnik on "How to check that model is right?" http://bbpress.tlaplus.net/topic/how-to-check-that-model-is-right#post-100 Wed, 12 May 2010 19:47:55 +0000 pdudnik 100@http://bbpress.tlaplus.net/ Hi, Sorry for so many posts. None of this is really urgent. I have a more high-level question. I started going through exercises from the README files. So far, I can write a model that passes the model checking. However, I am concerned that the model I write may not exactly be what I think it is. Since I have almost no experience with TLA+, it is hard for me to be sure even for simple examples that my specifications are correct. So, long story short, from what I understand the simulation mode is used to check that the specifications reflect my intentions. But I am not quite sure how to use the simulation mode, or at least how it is normally used. Should I insert some print statements and generate a trace and then manually go through it to make sure that the behavior is as expected? Or is there a better way? Thanks. Polina pdudnik on "A Caching Memory question" http://bbpress.tlaplus.net/topic/a-caching-memory-question#post-101 Thu, 13 May 2010 23:21:08 +0000 pdudnik 101@http://bbpress.tlaplus.net/ Hi, I have a question about Caching Memory. Specifically, I don't quite understand the atomicity of actions. So, for example is it possible for DoWr and MemQRd to be happening at the same time and interleave in some way? Or are these always linearized, meaning they cannot be both happening at the same time? So, is it assumed that all these transformations take no time and so one always happens after the other atomically? Because looking at DoRw and MemQRd I do not see conditions that would make them mutually exclusive and so prevent them from happening at the same time and accessing memQ at the same time. The reason I ask is because I am adding rdQ as dictated by the exercises section of the README file, and I am concerned about the access to that rdQ being atomic. Specifically, in order to satisfy the Coherence invariant, I have to make sure that the values in that rdQ don't violate it. There are two ways I see of doing that: 1) the easy way is to just make sure the rdQ is empty before doing the DoWr, 2) the other way is to update queues in addition to caches in DoWr. What I am worried about in both of these solutions, is that the new action I added to read from the rdQ will not be atomic with DoWr and will cause errors. Thank you. Polina Thanks. Polina