TLA+ | The way to specify

TLA+ | The way to specify » Recent Posts http://bbpress.tlaplus.net/ The TLA+ and PlusCal Resource en-US Wed, 22 Feb 2012 23:41:34 +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-171 Sun, 12 Feb 2012 00:12:37 +0000 CharpoV 171@http://bbpress.tlaplus.net/ No, I didn't know there was such a place. Leslie is aware of the bug, which has been around forever. I was just hoping it had been fixed at some point. MC Daniel Ricketts on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-170 Sat, 11 Feb 2012 23:24:37 +0000 Daniel Ricketts 170@http://bbpress.tlaplus.net/ You're absolutely right. Sorry about that. I was able to reproduce this bug in the Toolbox. Have you reported the bug at bugzilla.tlaplus.net ? CharpoV on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-169 Sat, 11 Feb 2012 22:01:10 +0000 CharpoV 169@http://bbpress.tlaplus.net/ No, it was not. The output in that case would have been: <code> Error: Deadlock reached. Error: The behavior up to this point is: ... </code> I had deadlock checking disabled, and the output from TLC was: <code> Checking temporal properties for the complete state space... Error: Temporal properties were violated. ... </code> where 'temporal properties' refers to Xshrinks. MC Daniel Ricketts on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-168 Sat, 11 Feb 2012 21:52:10 +0000 Daniel Ricketts 168@http://bbpress.tlaplus.net/ TLC also, by default, checks for absence of deadlock. The trace returned by TLC was not a counter example to P~> Q. It was a counter example to absence of deadlock. CharpoV on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-167 Sat, 11 Feb 2012 21:45:07 +0000 CharpoV 167@http://bbpress.tlaplus.net/ A counterexample to P ~> Q must be a trace in which a P state is followed by an infinite sequence of non-Q states. The counterexample produced by TLC is not valid because the trace has no P state. MC Daniel Ricketts on "Still the same old bug" http://bbpress.tlaplus.net/topic/still-the-same-old-bug#post-166 Sat, 11 Feb 2012 21:11:09 +0000 Daniel Ricketts 166@http://bbpress.tlaplus.net/ I don't believe that this is a bug. The trace given by TLC is a valid counterexample to deadlock-free execution. In state 4 of the trace, neither A nor B is enabled, so the system deadlocks. If you use the Toolbox, it's easy to see if you've disabled deadlock checking. You can also evaluate arbitrary expressions at all states of a trace to check, for example, if the next state actions are enabled. 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-164 Fri, 20 Jan 2012 09:47:22 +0000 groban 164@http://bbpress.tlaplus.net/ First of all I want to thank you for your time. I will try express better my questions. Question 1. In the HourClock example I deliberately modify the statement HCnxt == IF hr' # 12 THEN hr+1 ELSE 1 to the false statement HCnxt == IF hr' # 14 THEN hr+1 ELSE 1 in order to permit variable hr to take values 12,13 and see how the toolbox react and discover that the theorem HC => []HCini does not longer exist. However, I run the model and I see no difference from the previous example without the modification. Question 2. This question concerns the toolbox operation. I open toolbox and add the HourClock spec. I right click on the spec and select “Launch Prover…”. I click OK in the next window and an alert message appears saying that “Prover Launch has encountered a problem. The given Cygwin path c:/Cygwin/bin does not exist” My question is. I should install Cygwin in order to operate the prove tools included in toolbox? Finally, as new in TLA and toolbox I believe that it will be very helpful if there is tutorial (with a specific example-code) on how to write and prove a spec with toolbox (including error explanation etc) Thank you again! Leslie Lamport on "Hi - Newbee Question" http://bbpress.tlaplus.net/topic/hi-newbee-question#post-163 Thu, 19 Jan 2012 21:43:35 +0000 Leslie Lamport 163@http://bbpress.tlaplus.net/ I'm sorry that my reply was hard to read. Let's see if I can get this to be formatted in a reasonable way. <code> I'm afraid I don't know what you're trying to do. The definition HCnxt == IF hr' # 14 THEN hr+1 ELSE 1 makes no sense if HCnxt is supposed to be the next-state action. A formula should assert a meaningful sentence. For example, 2+2=4 says "two plus two equals four". Your definition of HCnxt is a formula that says If the value of hr in the next state does not equal 14, then the value of hr plus 1, else 1. That is not a meaningful sentence. If we are to figure out the problem you're having with the Toolbox, you will have to describe more precisely what you want to happen and exactly what you have done. </code> Leslie Lamport on "Hi - Newbee Question" http://bbpress.tlaplus.net/topic/hi-newbee-question#post-162 Thu, 19 Jan 2012 21:41:04 +0000 Leslie Lamport 162@http://bbpress.tlaplus.net/ I'm afraid I don't know what you're trying to do. The definition HCnxt == IF hr' # 14 THEN hr+1 ELSE 1 makes no sense if HCnxt is supposed to be the next-state action. A formula should assert a meaningful sentence. For example, 2+2=4 says "two plus two equals four". Your definition of HCnxt is a formula that says If the value of hr in the next state does not equal 14, then the value of hr plus 1, else 1. That is not a meaningful sentence. If we are to figure out the problem you're having with the Toolbox, you will have to describe more precisely what you want to happen and exactly what you have done. 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 hansen 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-159 Thu, 10 Nov 2011 14:18:54 +0000 hansen 159@http://bbpress.tlaplus.net/ The error is being caused by the precedence of the "IF THEN ELSE" construct. The "ELSE" clause has the lowest possible precedence and ends only after the "UNCHANGED" statement (see Specifying Systems, chapter 15.2.1: Undelimited Constructs). To fix the error you have to put the whole "IF THEN ELSE" construct in brackets: ... BootRom_state' =(IF BootRom_corrupt=0 THEN "malicious" ELSE "good") /\ ... 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? Leslie Lamport on "TLA+ Specification" http://bbpress.tlaplus.net/topic/tla-specification#post-157 Mon, 26 Sep 2011 14:25:35 +0000 Leslie Lamport 157@http://bbpress.tlaplus.net/ The first thing you should do is read about TLA and TLA+. See the Documentation/Books page. You will discover that TLA+ is not a programming language. Perhaps you want PlusCal. 1) PlusCal contains a print statement, but it's mostly for debugging. You are more likely to want to check that, at some point in your PlusCal code, x = y!, for some variables x and y. To do that, you would define Factorial in TLA+ and add the assertion x = Factorial(y). 2) You just don't tell TLC to check any liveness property. Leslie Lamport 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. Leslie Lamport on "Creating a Sequence from a Set?" http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set#post-154 Thu, 15 Sep 2011 11:27:41 +0000 Leslie Lamport 154@http://bbpress.tlaplus.net/ Laven writes that his definition of ToSeq produces a sequence in the reverse order than that produced by Merz's definition. What he should have written is that this was what he discovered when running the two definitions on a particular example on a particular version of TLC. The semantics of TLA+ do not imply this, and what those definitions produce could depend on the particular version of the particular tool one is using. If you want the elements in a certain order, you should define an operator that ensures that they are in that order--for example, one that sorts the sequence produced by either Laven's or Merz's definitiion. mkuppe on "Nullpointerexception" http://bbpress.tlaplus.net/topic/nullpointerexception#post-153 Thu, 15 Sep 2011 11:22:12 +0000 mkuppe 153@http://bbpress.tlaplus.net/ Hi mkoconnor, what does the actual stack trace look like? Can you post it here? Since you are on Mac, you might be hit by bug #111 (<a href="https://bugzilla.tlaplus.net/show_bug.cgi?id=111" rel="nofollow">https://bugzilla.tlaplus.net/show_bug.cgi?id=111</a>) which is going to be fixed in the next Toolbox release. Markus Laven on "Nullpointerexception" http://bbpress.tlaplus.net/topic/nullpointerexception#post-152 Thu, 25 Aug 2011 08:46:09 +0000 Laven 152@http://bbpress.tlaplus.net/ I saw the same problem in Simulation mode, but not in Model-checking mode. But looks it doesn't affect the results. Laven on "Creating a Sequence from a Set?" http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set#post-151 Thu, 25 Aug 2011 08:43:50 +0000 Laven 151@http://bbpress.tlaplus.net/ I wrote it this way: ToSeq(S) == LET M == Cardinality(S) IN CHOOSE x \in [1..M->S]:Cardinality({x[n]:n \in (1..M)}) = M It creates a reverse order seq compare to merz's recursive solution. 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! 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 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.) Leslie Lamport 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-147 Wed, 22 Jun 2011 07:56:12 +0000 Leslie Lamport 147@http://bbpress.tlaplus.net/ <pre><code>CORRECTION. I did not meant to say that this web site is crappy. I was referring to the software used to create the web pages. (I presume it was the best free software available when the site was created.) We are doing the best we can to produce a good web site with this crappy software. Please excuse us if we are slow to respond to postings. There are few of us and we are very busy. I have turned my comments above into a module showing a few ways to define the transitive closure. It will appear in the examples directory in the next release of the TLA+ tools.</code></pre> 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. Leslie Lamport on "Possible bug in TLC?" http://bbpress.tlaplus.net/topic/possible-bug-in-tlc#post-145 Tue, 21 Jun 2011 11:24:40 +0000 Leslie Lamport 145@http://bbpress.tlaplus.net/ <code>Thanks for the report. We will check it out.</code> Leslie Lamport 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-144 Mon, 20 Jun 2011 17:47:32 +0000 Leslie Lamport 144@http://bbpress.tlaplus.net/ Sorry, I forgot that this crappy web site doesn't allow you to type readable posts. To get a readable version, copy this posting into a sensible text editor and replace every @ with a space. @@@@@@ @@@@@@ If R is a relation--that is a set of ordered pairs--let its support be the set of all elements that appear in those pairs. Then R defines a directed graph on its support, where there is an edge from s to t iff <<s, t>> is in R. The closure of R is the set of all pairs <<s, t>> such that s and t are in the support of R and there is a path from s to t. @@@ This leads to the following definition of the closure: @@@ Support(R)@==@{r[1]@:@r@\in@R}@\cup@{r[2]@:@r@\in@R} @@@ Closure(R)@==@ @@LET@S@==@Support(R) @@IN@@{<<s,@t>>@\in@S@\X@S@:@\E@p@\in@Seq(S)@:@/\@Len(p)@>@1 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@p[1]@=@s @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@p[Len(p)]@=@t @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@/\@\A@i@\in@@1..(Len(p)-1)@: @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@<<p[i],@p[i+1]>>@\in@R} @@@ This can't be evaluated by TLC because Seq(S) is an infinite set. However, it's not hard to see that it suffices to consider paths whose length is at most Cardinality(S). I'll let you modify the definition to one that TLC will be able to evaluate. @@@ However, the naive evaluation that TLC uses makes this definition rather inefficient. (As an exercise, find an upper bound on its complexity.) A definition that TLC can evaluate more efficiently is obtained by recursively defining the function C with domain Nat such that C[n] the set of all pairs <<s, t>> with s, t \in Support(R) such that there exists a path of length at most n+1 from s to t in Support(R), and then define Closure(R) to equal C[Cardinality(Support(R))-1]. @@@@ To check your definitions, define Closure1 and Closure2 with these two definitions, and have TLC check @@@@@ @@@ASSUME@\A@N@\in@0..3@:@\A@R@\in@SUBSET@((1..N)@\X@(1..N))@:@ @@@@@@@@@@@@@@@Closure1(R)@=@Closure2(R) Leslie Lamport 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-143 Mon, 20 Jun 2011 17:40:56 +0000 Leslie Lamport 143@http://bbpress.tlaplus.net/ If R is a relation--that is a set of ordered pairs--let its support be the set of all elements that appear in those pairs. Then R defines a directed graph on its support, where there is an edge from s to t iff <<s, t>> is in R. The closure of R is the set of all pairs <<s, t>> such that s and t are in the support of R and there is a path from s to t. This leads to the following definition of the closure Support(R) == {r[1] : r \in R} \cup {r[2] : r \in R} Closure(R) == LET S == Support(R) IN {<<s, t>> \in S \X S : \E p \in Seq(S) : /\ Len(p) > 1 /\ p[1] = s /\ p[Len(p)] = t /\ \A i \in 1..(Len(p)-1) : <<p[i], p[i+1]>> \in R} This can't be evaluated by TLC because Seq(S) is an infinite set. However, it's not hard to see that it suffices to consider paths whose length is at most Cardinality(S). I'll let you modify the definition to one that TLC will be able to evaluate. However, the naive evaluation that TLC uses makes this definition rather inefficient. (As an exercise, find an upper bound on its complexity.) A definition that TLC can evaluate more efficiently is obtained by recursively defining the function C with domain Nat such that C[n] is the set of all pairs <<s, t>> with s, t \in Support(R) such that there exists a path of length at most n+1 from s to t in Support(R), and then define Closure(R) to equal C[Cardinality(Support(R))-1]. To check your definitions, define Closure1 and Closure2 with these two definitions, and have TLC check ASSUME \A N \in 0..3 : \A R \in SUBSET ((1..N) \X (1..N)) : Closure1(R) = Closure2(R) Hilleman on "Measuring memory usage" http://bbpress.tlaplus.net/topic/measuring-memory-usage#post-142 Sat, 18 Jun 2011 09:53:44 +0000 Hilleman 142@http://bbpress.tlaplus.net/ I want to know how much memory was used after the model checker has run. In other model checkers like Uppaal we can check how much memory was used after a query has processed. <a href="http://www.ebelow.com/ipad-2-chargers.html">ipad2 Chargers</a> <a href="http://www.ebelow.com/ipad-2-pouch-cases.html">iPad 2 Pouch Case</a> <a href="http://www.ebelow.com/ipad-2-soft-cases.html">ipad 2 Soft case</a> 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. giuliano on "Possible bug in TLC?" http://bbpress.tlaplus.net/topic/possible-bug-in-tlc#post-140 Fri, 15 Apr 2011 09:50:29 +0000 giuliano 140@http://bbpress.tlaplus.net/ Hello, I simplified a bit the example: File Test.tla: <pre><code>------------------------ MODULE Test ------------------------ CONSTANTS X VARIABLES y ----------------------------------- Init == y = {} Z == {z \in [{0} -> {0}] : \E x \in X : FALSE} Next == y' = Z ==============================</code></pre> File MCTest.tla: <pre><code>-------------------- MODULE MCTest -------------------------------- X == {} VARIABLES y I == INSTANCE Test Next == I!Next Init == I!Init ============================</code></pre> File MCTest.cfg: <pre><code>INIT Init NEXT Next</code></pre> Given those files, the command "java -cp ~/tla/tla/ tlc2/TLC MCTest.tla" outputs: <pre><code>TLC2 Version 2.03 of 10 March 2011 Running in Model-Checking mode. Parsing file MCTest.tla Parsing file Test.tla Semantic processing of module Test Semantic processing of module MCTest Starting... (2011-04-15 10:49:44) Computing initial states... Finished computing initial states: 1 distinct state generated. Error: In evaluation, the identifier X is either undefined or not an operator. line 11, col 37 to line 11, col 37 of module Test Error: The behavior up to this point is: State 1: <Initial predicate> y = {} Error: The error occurred when TLC was evaluating the nested expressions at the following positions: 0. Line 11, column 37 to line 11, column 37 in Test 3 states generated, 1 distinct states found, 0 states left on queue. The depth of the complete state graph search is 1. Finished. (2011-04-15 10:49:44)</code></pre> Line 11 contains <code>Z == {z \in [{0} -> {0}] : \E x \in X : FALSE}</code> robson on "WildFire Challenge and TLA+ ToolBox" http://bbpress.tlaplus.net/topic/wildfire-challenge-and-tla-toolbox#post-139 Tue, 12 Apr 2011 18:24:45 +0000 robson 139@http://bbpress.tlaplus.net/ Hi Stephan, thanks for you help. I'll check this more carefully. 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 merz on "WildFire Challenge and TLA+ ToolBox" http://bbpress.tlaplus.net/topic/wildfire-challenge-and-tla-toolbox#post-137 Tue, 12 Apr 2011 11:51:04 +0000 merz 137@http://bbpress.tlaplus.net/ Hi, indeed TLC cannot evaluate unbounded CHOOSE expressions, i.e. CHOOSE x: P(x). See the TLC documentation: only bounded quantification over finite sets is supported, such as \A x \in S: P(x) or CHOOSE x \in S: P(x), where S is a finite set. By the way, Wildfire was not originally intended for model checking -- you would have to rewrite the model to make it amenable to (finite-state) model checking. Best regards, Stephan