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.

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.