1

Question

When using CLI, how to have it show n-th level action trace name (and symbolic arguments names) when an error occurs?

Command: java -jar tla2tools.jar Test.tla

Normal

For example, with:

Spec == Init /\ [][Next]_<<AllStates>>

it shows:

State 1: <Initial predicate>
...
State 2: <BuyComputer line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <BuyHouse line 17, col 3 to line 17, col 55 of module Test>
...

With condition

and with (if total cost is greater than 100, then do not visit state):

Spec == Init /\ [][Next /\ ((cost' > 100) => UNCHANGED <<AllStates>>)]_<<AllStates>>

it shows:

State 1: <Initial predicate>
...
State 2: <Action line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <Action line 17, col 3 to line 17, col 55 of module Test>
...

The Action should be BuyComputer and BuyHouse.

Desired with condition

State 1: <Initial predicate>
...
State 2: <BuyComputer(Me) line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <BuyHouse(Neighbour) line 17, col 3 to line 17, col 55 of module Test>
...

with the functions defined as BuyComputer(who) == ... and BuyHouse(who) == ....

Why

I'm trying to cut down the number of visited states where I know won't lead to an error. In this case, it is when cost > 100. I also want the action name instead of "unnamed action" for easier debugging.

jmpsabisb
  • 182
  • 1
  • 10
  • You didn't share your Next predicate but usually this is a disjunction of actions, where actions are usually conjunctions of the form `x' = F(x)`. My attempt would be to use `[cost <= 100 /\ Next]_<>` - a simplification of `[(cost <= 100 /\ Next) \/ (cost > 100 /\ UNCHANGED(vars)]_<>` because the `_<>` is a shortcut for `\/ UNCHANGED(vars)` anyway. I haven't tried this in the toolbox though. – lambda.xy.x May 15 '23 at 21:03
  • Your text sounds like you want to look at small traces but I'm not sure if that's correct. To ensure a minimal length of the trace, I'd replace the invariant `INV` to check with `count > 100 => INV ` but keep Spec in the standard form. – lambda.xy.x May 15 '23 at 21:06
  • @lambda.xy.x missed a parenthesis when changing to one line (edited post). Are you suggesting I simply swap `Next /\ (condition => UNCHANGED)` to `(condition => UNCHANGED) /\ Next`? It still shows up as an unnamed action this way. It works fine if it's just `Next` (without `/\ (condition => UNCHANGED)`). – jmpsabisb May 15 '23 at 21:45
  • My `Next` is the usual disjunction of actions (`Next == ActionA \/ ActionB \/ ActionC ` where `ActionA == VarX' = VarX + 1`). And you're right, I am looking at small traces (under 50 actions). – jmpsabisb May 15 '23 at 21:46
  • `count > 100 => INV`: I assume you mean `cost <= 100 => INV`? Even still, this does not reduce the number of visited states (there's no reason to continue to `BuyComputer` when `cost = 120` and `budget = 100` for example). – jmpsabisb May 15 '23 at 21:52

1 Answers1

1

Sorry for misleading you a bit in the comments - I only realized afterwards, that you want the action names in the trace. As far as I understand, this works only if Next is a disjunction of Operator Definitions. I've just made a small toy example:

EXTENDS Naturals, TLAPS

VARIABLES x, y

Init == x = 0 /\ y = 0
AddOne(v, w) == v' = v + 1 /\ w' = w + 1
AddTwo(v, w) == v' = v + 2 /\ w' = w + 1
Next == AddOne(y,x) \/ AddTwo(y,x)

Spec == Init /\ [][Next]_<<x,y>> /\ WF_x(Next)

INV == x \in 2 .. 5 => y < 6

I assume weak fairness of Next to avoid infinite stuttering traces. I've also explicitly added the definition INV for the invariant, such that it is easier to enter into the model checking properties. The variable y may be increased by one or two whereas x just traces the number of steps taken.

Instead of modifying Next it's actually better to put the conidtion into the invariant to check. Obviously, y < 6 is always invalidated after six steps. But since the invariant is guarded with x \in 2 .. 5 it has to be invalidated in that number of steps. Since Next was not altered the actions occur in the trace as expected:

Invariant INV is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ x = 0
/\ y = 0
2: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 1
/\ y = 2
3: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 2
/\ y = 4
4: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 3
/\ y = 6

Is that what you wanted to solve? In my opinion, putting the condition into the invariant is also better because the specification is unmodified. Otherwise it's not clear if the modifications lead to that particular safety property violation.

Edit: Since we want to cut down the states, we need to change Next. I introduced a predicate Limit(P,N) that limits the application of Next to the cases where x < N.

Limit(P, N) == (x < N) /\ P
Spec2 == Init /\ [][Limit(Next, 4)]_<<x,y>> /\ WF_x(Next)

Model checking Spec finds the trace visiting 22 states (16 distinct), model checking Spec2 visits 18 states (13 distinct). I would expect that those are the states where x is 4 or larger.

Edit2: If you want the names in the trace you need to add definitions that can be named in the trace. E.g.:


LAddOne(v,w) == Limit(AddOne(v,w),4) 
LAddTwo(v,w) == Limit(AddTwo(v,w),4)
LNothing == x >= 5 /\ UNCHANGED <<x,y>>

Next3 == LAddOne(y,x) \/ LAddTwo(y,x) \/ LNothing
Spec3 == Init /\ [][Next3]_<<x,y>> /\ WF_x(Next)

There was also a bug in Spec and Spec2 where we had only [][Next]_x instead of [][Next]_<<x,y>> leading to involuntary deadlock in some cases. I fixed it.

lambda.xy.x
  • 4,918
  • 24
  • 35
  • "Is that what you wanted to solve?": I don't think it does (see Why section in post: "I'm trying to cut down the number of visited states". It being turned into an unnamed action is an unwanted side effect). In your example, having `INV == x \in 2 .. 5 => y < 6` (your suggestion) and `INV == y < 6` (similar to what I have originally) both lead to the same number of visited states, even with `AddHalf(v, w) == v' = v + 1 /\ w' = w + 2` and `Next == ... \/ AddHalf(y,x)`. – jmpsabisb May 16 '23 at 17:14
  • Hm, in principle TLC does a breadth first search on the states (with lots of optimizations) so you really need to change the spec. Then I don't have many ideas but to have two kinds of Next depending on depth. It still only cuts of states after that depth is reached. – lambda.xy.x May 16 '23 at 21:52
  • For your updated post (`[][Limit(Next, 4)]_x` where `Limit(P, N) == (x < N) /\ P`), is it not the same as what I have in my post (`[][Next /\ ((cost' > 100) => UNCHANGED <>)]_<>`)? The problem with this is that it shows up as an unnamed action in the trace. – jmpsabisb May 16 '23 at 22:16
  • Yes, it's a different spec with different actions. The trace shows you the disjuncts of Next, so you would need to introduce new definitions and distribute the Limit to each disjunct. – lambda.xy.x May 16 '23 at 22:28
  • Hm still get a deadlock, need to fix again. – lambda.xy.x May 16 '23 at 22:32
  • Your edit 2 is what I used before I posted . Since I didn't add it to my post, I will mark your post as correct answer soon. I hoped for there to be a less hacky workaround. – jmpsabisb May 16 '23 at 22:38
  • Ah I see - yeah, if you want the actions named there's not much choice (just careful with the the implication in `cost < 4 => UNCHANGED cost` since it's equivalent to `cost >= 4 \/ UNCHANGED cost` but you would want to have a conjunction there and add this as another action -- see the LNothing action I needed to add to distinguish accidental deadlock from intentional one.) – lambda.xy.x May 16 '23 at 22:42