hwayne / learntla Goto Github PK

Error message:

The `Evaluate Constant Expression� section�s evaluation failed.
Attempted to check equality of string "a" with non-string:
2

I've tested in TLA+ Toolbox 1.6.0 using expression ("No Behavior Spec"):

LET chessboard_squares == {"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8)
IN 
/\ <<"a", 2>> \in chessboard_squares
/\ <<2, "a">> \notin chessboard_squares
/\ <<"b", 10>> \notin chessboard_squares

Removing <<2, "a">> fixes the expression.

In the appendix, the reference section claims:

(CHOOSE x \in {1, 2, 3} : x <= 2) = \* 1 or 2, arbitrary

However, looking at this thread, I'm lead to believe that CHOOSE will always return the same value, which I believe should be 1 if evaluated by TLC.

Maybe the point from the hyperbook should be emphasized:

In mathematics, there is no such thing as a nondeterministic operator
or a nondeterministic function. If some expression equals 42 today, then
it equaled 42 yesterday and it will still equal 42 next year. [...] The
semantics of TLA + do not specify which value in 1.. 10; but it is the
same one every time.

See https://www.reddit.com/r/tlaplus/comments/bsvdnp/is_tlc_really_breadthfirst_search/

Use \union and \intersect instead for consistency

The text says,

add x /= 6 to the “Invariants” section

... but the screenshot shows "x # 6".

On https://learntla.com/tla/tuples/ it says

Structures are hashes. They have keys and values. You specify them as [key |-> value] and query them with either [key] or .key. Both are legal and valid.

Structures are for when you have fixed data, while with hashes you can have mutable data. You should be arbitrarily adding and removing keys from a structure.

Example of confusion: https://stackoverflow.com/questions/47115185/tla-how-to-delete-structure-key-value-pairings

Working through the examples one by one, I found I couldn't complete the Twople exercise. I came across 2 problems:

1. I had to peek at the answer of how to reverse a two tuple. I did not know how to raise an error at this point in TLA+, so maybe you should consider introducing this earlier on?

2. The supplied solution didn't work for me when I pasted it into the toolbox (I may be doing something wrong here).

Spec

---------------------------- MODULE LearnTlaPlus ----------------------------
EXTENDS Integers, Sequences
                      
Reverse(Twople) == IF Len(Twople) = 2 THEN <<Twople[2], Twople[1]>> ELSE ASSERT FALSE
               
=============================================================================

Error (truncated for brevity as it's impossible to copy/paste the parse errors on OSX)

***Parse Error***
Was expecting  "==== or more Module body"
Encountered FALSE at ...

@markrwilliams upgraded theme in #30, what can we do to expand the guide?

On https://www.learntla.com/pluscal/behaviors/

Does not follow label rules from https://www.learntla.com/concurrency/labels/ so is invalid. See https://twitter.com/aphyr/status/927652007594352640

https://github.com/hwayne/learntla/blob/master/content/introduction/example/index.md#L34

:(

The example below (copied from https://learntla.com/pluscal/behaviors/) is bogus and future Pcal translator versions won't accept it (see screenshot below). The "f" in the either statement is a bound identifier and thus cannot be assigned a value.

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables f1 \in BOOLEAN, f2 \in BOOLEAN, f3 \in BOOLEAN
begin
  while TRUE do
    with f \in {f1, f2, f3} do
      either
        f := TRUE;
      or
        f := FALSE;
      end either;
    end with;
  end while;
end algorithm; *)

====

The link TLA+ Toolbox in the first paragraph of https://learntla.com/pluscal/toolbox/ is dead (400 Bad Request). I'm not sure what was there before but maybe it can be replaced with http://lamport.azurewebsites.net/tla/toolbox.html?

TODO explain why this is something I want to do

People often seem to get tripped up by the semantics of what a deadlock is in TLA+ and how TLC checks for it. For example, see this thread and this thread. To help avoid the same confusion for others in future, might help to include a more explicit section covering the notion of deadlock in TLA+. A note does appear here in the section on processes, but it might be easy to miss if you're looking for details about deadlocks specifically.

Hi @hwayne, not sure if anyone is watching the practical TLA+ repository, but it's missing the PT library advertised in the book

Apress/practical-tla-plus#1

Thanks!

Looking at the site itself (https://www.learntla.com/introduction/), it says in the upper-left corner:

This work is licensed under a Creative Commons Attribution 4.0 International License.

So you probably want to add the contents of this URL as the file LICENSE in your repo so that it's obvious and GitHub will recognize it and mark the repo as such.

Without having a license file, it's unclear to folks who only see the GitHub repo and not the site what the license of the repo's content is, and whether or not they can contribute patches or reuse the content — which, in the absence of a license, they cannot by default — the absence of a license implies "all rights reserved", at least in some countries.

https://www.learntla.com/models/constants/ should link to https://www.learntla.com/tla/tuples/

The implementation of IsSensical() assumption given in "Models->Constants" section won't catch the problem with TSPACES <- 3, TSIZE <- 3, SOLUTION <- <<<<1,2>>, <<>>, <<3,4>>>> which is the example you are discussing in this section.

So, instead of:

IsSensical(state) == /\ Len(state) = TSPACES \* Correct spaces
                     /\ \A n \in 1..TSIZE : \* All numbers appear
                        \E tower \in DOMAIN state:
                            \E disc \in DOMAIN state[tower]:
                                n = state[tower][disc] 

it's better to use the following:

  IsSensical(state) ==  /\ Len(state) = TSPACES \* Correct spaces
                        /\ \A tower \in DOMAIN state: \* Numbers do not exceed TSIZE
                            \A disc \in DOMAIN state[tower]:
                                state[tower][disc] \in 1..TSIZE
                        /\ \A n \in 1..TSIZE : \* All numbers appear
                            \E tower \in DOMAIN state:
                                \E disc \in DOMAIN state[tower]:
                                    n = state[tower][disc] 

I was about to open an issue that https://learntla.com/introduction/about-this-guide/ points to an outdated version of the PlusCal manual, however, 49a0b46 fixed this problem.

Yet, still, the link for me points to https://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html

I tried Ctrl+Shift+R-refreshing the page.

\E x, y \in 1..10: x > y \* TRUE
\A x, y \in 1..10: x > y \* FALSE
CHOOSE x, y \in 1..10: x > y \* Error

Didn't know the first two forms were possible! Thought you had to do \A x \in S, y \in S.

When I try to execute the spec at the bottom of the Behaviors page, I get an error. Here's the spec:

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables flags = [1..3 -> BOOLEAN], next = TRUE;
begin
  while next do
    with f \in DOMAIN flags, n \in BOOLEAN do
      flags[f] := ~flags[f];
      next := n;
    end with;
  end while;
end algorithm; *)

====

and here's the error I got after running the model checker:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply the operator DOMAIN to a non-function
(a set of the form [S -> T])

When I evaluate [1..3 -> BOOLEAN], its value is

{ <<FALSE, FALSE, FALSE>>,
     <<FALSE, FALSE, TRUE>>,
     <<FALSE, TRUE, FALSE>>,
     <<FALSE, TRUE, TRUE>>,
     <<TRUE, FALSE, FALSE>>,
     <<TRUE, FALSE, TRUE>>,
     <<TRUE, TRUE, FALSE>>,
     <<TRUE, TRUE, TRUE>> }

So I see that flags a set, not a function, which explains the error "Attempted to apply the operator DOMAIN to a non-function". I'm not sure what's the proper way to make flags a function for the three boolean flags.

This section suggests to define an operator

Five == 5
Five + 5 \* 10

However, it doesn't specify (can't find?) where to enter that expression? I have tried in "Evaluate Constant Expression", and throws a parsing error. I also tried to put it into "spec.tla" file, between begin and end algorithm, which throws an Unrecoverable Error. I ve also tried to put it after end algorithm, but nothing in there seems to be taken into account

The page on operators contains an example that features a higher-order recursive operator, which is illegal. I know it was deemed more of a happy coincidence and remains untouched for now, but it gets confusing if you write specs like

RECURSIVE Bug(_,_)
Bug(a,b(_)) == 1

which is not covered by the bug and produces an error message, which I in turn thought was a bug until I realized that HOROs are illegal in the first place. Apparently, there's a bug in the bug. To avoid such confusion it would be nice if the page would contain a short note that HOROs are a bug / not actually supported.
Suggestion:

{{% notice note %}} While technically TLA+ does not permit recursive higher-order operators (like the one above) TLC partially supports them due to a bug {{% /notice %}}

I know it was filed by the author of the page, but for the sake of completeness: tlaplus/tlaplus#57

My understanding is that you are working on an overhaul of this site, so I am posting this note as a possible feature you might be interested in including in the next version.

The tla-web tool implements a fully browser based TLA+ evaluator/interpreter. It might be cool for certain pages of the site to embed interactive/executable TLA+ specs/snippets inline. The Lean theorem prover tutorials have something similar.

The current version of the tool probably isn't quite suitable for embedding elsewhere yet, but it shouldn't be hard to make a simple interface/API to allow this. Just thought I'd make you aware of this as a possibility.

This is the specific page:
https://www.learntla.com/introduction/example/

After adding in the process I'm getting the error

Attempted to apply the operator overridden by the Java method
public static tlc2.value.BoolValue tlc2.module.Naturals.GEQ(tlc2.value.Value,tlc2.value.Value),
but it produced the following error:

The first argument of > should be an integer, but instead it is:
<<1, 1>>


While working on the initial state:
/\ bob_account = 10
/\ money = <<1, 1>>
/\ alice_account = 10
/\ pc = <<"Transfer_", "Transfer_">>
/\ account_total = 20

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 29, column 9 to line 34, column 50 in transfer
1. Line 29, column 12 to line 29, column 29 in transfer
2. Line 30, column 12 to line 30, column 27 in transfer
3. Line 31, column 12 to line 31, column 54 in transfer
... Omitted for brevity ...
1597. Line 34, column 17 to line 34, column 50 in transfer
1598. Line 34, column 27 to line 34, column 33 in transfer
1599. Line 34, column 39 to line 34, column 49 in transfer

Here is my full tla file:

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10,
          account_total = alice_account + bob_account;

process Transfer \in 1..2
  variable money \in 1..20;
begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
       bob_account := bob_account + money;
end if;
C: assert alice_account >= 0;
end process

end algorithm *)
\* BEGIN TRANSLATION
\* Label Transfer of process Transfer at line 12 col 3 changed to Transfer_
VARIABLES alice_account, bob_account, account_total, pc, money

vars == << alice_account, bob_account, account_total, pc, money >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ alice_account = 10
        /\ bob_account = 10
        /\ account_total = alice_account + bob_account
        (* Process Transfer *)
        /\ money \in [1..2 -> 1..20]
        /\ pc = [self \in ProcSet |-> "Transfer_"]

Transfer_(self) == /\ pc[self] = "Transfer_"
                   /\ IF alice_account >= money[self]
                         THEN /\ pc' = [pc EXCEPT ![self] = "A"]
                         ELSE /\ pc' = [pc EXCEPT ![self] = "C"]
                   /\ UNCHANGED << alice_account, bob_account, account_total, 
                                   money >>

A(self) == /\ pc[self] = "A"
           /\ alice_account' = alice_account - money[self]
           /\ bob_account' = bob_account + money[self]
           /\ pc' = [pc EXCEPT ![self] = "C"]
           /\ UNCHANGED << account_total, money >>

C(self) == /\ pc[self] = "C"
           /\ Assert(alice_account >= 0, 
                     "Failure of assertion at line 16, column 4.")
           /\ pc' = [pc EXCEPT ![self] = "Done"]
           /\ UNCHANGED << alice_account, bob_account, account_total, money >>

Transfer(self) == Transfer_(self) \/ A(self) \/ C(self)

Next == (\E self \in 1..2: Transfer(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

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

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

====

Is there some sort of problem in how I wrote my specification?

Hi, I'm going through this example:

https://learntla.com/introduction/example/

but I cannot get the IDE to parse account total. I copied and pasted the example.

variables alice_account = 10, bob_account = 10, money \in 1..20,
          account_total = alice_account + bob_account;

begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
       bob_account := bob_account + money; \* Both now part of A
end if;
C: assert alice_account >= 0;

end algorithm *)

\* BEGIN TRANSLATION
\* removed..
\* END TRANSLATION

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

See #10

Hi! Me again.

On the final step of the "Using the Toolbox" section you are instructed to add the following string to the "Evaluate Constant Expression" section of the "Model Checking Results" tab:

CHOOSE x \in {1, 2, 3} : x*x = 4

However, upon doing so I get the following error:

Multiply-defined symbol 'x': this definition or declaration conflicts with the one at line 11, col 11 to line 11, col 11 of module integers.

Changing to code to use the y variable results in the correct response of 2.

CHOOSE y \in {1, 2, 3} : y*y = 4

It appears that the definition of x in "Evaluate Constant Expression" conflicts with the value of x in the PLUSCAL algorithm. And the tutorial could be fixed by either instructing the user to remove the code from their algorithm or change the new definition to use the variable y instead of x.

srsly, it's been like two years

Maybe set an official start date of October or something

The section on infinite loops discusses the concept of DFS but State Constraints are much better suited to to restrict the state space. E.g. in the example at hand, a state constraint such as "x < 42" would be a good illustration. That's a) easier to come up with compared to 7 and b) is less blunt than simply pruning the state graph.

When performing on set containing duplicated elements, I found that with only creates a behavior for each distinct element in the set.
with a \in {1, 1, 2,2, 3,3} do print a; end with
The output will be: 1, 2, 3
Is my understanding right? If so, I think it's better to emphasize this behavior.

3c7fd58#commitcomment-22320853

I've taken the model from here and run it with only 1 philosopher.

Supposedly this should work just fine. When I run it, I end up with "Deadlock reached." Here is the Error Trace

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 forks |-> <<0>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"P">>
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "P",
   location |-> "line 64, col 12 to line 71, col 30 of module Playground"
 ],
 forks |-> <<1>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"Eat">>
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Eat",
   location |-> "line 73, col 14 to line 80, col 47 of module Playground"
 ],
 forks |-> <<1>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"P">>
]
>>

The tower of hanoi example uses the || when it hasn't been introduced (I'm not sure if it is later). It then goes on to say "Everything should look familiar with the exception of the set syntax we use to define “from” and “to”".
A short parenthetical would help – something like "(and the || operator, which lets multiple assignments all use the old values)"

in the InSensical declaration on the Models->Constraints page, you use ‘tower’ as a variable name scoped to the declaration, but in the larger context of the Hanoi problem, the variable ‘tower’ already has been defined global to the spec which seems like it should make the parser unhappy.

Not a bug, just confusing

https://learntla.com/models/constants/

https://twitter.com/Hillelogram/status/880198270068424704

Basically

/\ A
/\ B
  => C

is A /\ (B => C), not A /\ B => C as expected (you'd need to deindent => to get that)

Should also let people know this in the guide to avoid any other mistakes

On the operators page there is this reminder:

Remember, you can use the “No Behavior Spec” option in your TLC model to test various operators and cases.

Which conceptually makes sense, but if I try to put the operator definition (Neq(a,b) == a /= b ) directly in the "Evaluate Constant Expression" section then I get an error. Similarly if I put the operator definition in the PLUSCAL algorithm I get a compilation error. I suppose this is because an operator is a TLA+ concept rather than a PLUSCAL concept.

But at this point in the tutorial we haven't written any actual TLA+ code yet and I'm a bit unsure how to best do so. I can add the operator definition in the middle of the TLA+ block but that wouldn't be the best place since it will get overridden upon the next PLUSCAL translation. I guess the best place would be before or after the BEGIN TRANSLATION or END TRANSLATION statements?

By the way I'm very much enjoying the tutorial so far. I'm asking these questions to further my edification as well as improve the tutorial for everyone else. For this particular issue I think that either I'd remove the tip block or add a new section that will actually run the user through adding an operator definition to their TLA file (and telling them where it should go).

The external reading material listed on https://learntla.com/introduction/about-this-guide/ is bundled with the TLAToolbox version 1.5.4 onwards. You might want to inform readers.

The exercise on https://learntla.com/tla/logic/ that follows the explanation of "=> and <=>" requires this answer:

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

This is confusing, because the section has explained logic operators, but the exercise is about the mathematical comparison "<=" (less than or equal to).

it would be nice if the guide included a link (preferably direct) to downloading the IDE and proof system:

• http://lamport.azurewebsites.net/tla/toolbox.html
• http://tla.msr-inria.inria.fr/tlaps/content/Home.html

It felt like a chore to dig out the right links to download the tools.

See #18 (comment)

https://learntla.com/tla/sets/

InSeqSets(elem, Seq) == x \in UNION Range(Seq)
-----------------------
\/ InSeqSets(elem, Seq) == elem \in UNION Range(Seq)
\/ InSeqSets(x, Seq) == x \in UNION Range(Seq)

See 12703bb

LargestTwinPairRef(S) == CHOOSE <<x, y>> \in S \X S:
                         /\ IsPrime(x)
                         /\ IsPrime(y)
                         /\ x = y - 2
                         /\ \A <<w, z>> \in S \X S:
                            /\ IsPrime(z)
                            /\ IsPrime(w)
                            /\ w = z - 2
                            => z < y

PrintVal(id, exp)  ==  Print(<<id, exp>>, TRUE)
ASSUME PrintVal("LargestTwinPairRef", LargestTwinPairRef({3, 5, 13}))

(see https://learntla.com/tla/logic/)

Produces

Evaluating assumption line 72, col 8 to line 72, col 54 of module hw failed.
Attempted to compute the value of an expression of form
CHOOSE x \in S: P, but no element of S satisfied P.
line 54, col 25 to line 62, col 36 of module hw

It should be z <= y