Re: Model evaluator forgetting about state variable

[rws...@xxxxxxxxx]

On Friday, August 14, 2015 at 7:36:47 AM UTC-4, rws...@xxxxxxxxx wrote:
> I've been editing a fairly complicated (for me, at least) specification across multiple modules. This is happening on a Linux box with Oracle Java 1.8 and toolkit 1.5.1. One of the modules starts as follows:
> 
> === start fragment
> ------------------------ MODULE ObjectWithEventsCrud ------------------------
> EXTENDS EnumeratedField
> 
> LOCAL INSTANCE Integers
> LOCAL INSTANCE Sequences
> LOCAL INSTANCE TLC
> LOCAL INSTANCE GlobalConstants
> 
> VARIABLE objectStore
> === end fragment
> 
> Further down in the spec there's the following operator (Print statements are there because I'm trying to figure out what's going on):
> === start fragment
> \* ============= STEPS ===================
> \* Add an object to the objectStore
> createObjectInEmpty(objectId, noHistoryFunction) ==
>   /\ Print("CRUD create object empty legal",LegalNoHistory(noHistoryFunction))
>   /\ Print("CRUD create object empty id",objectId \in ObjectIdSet)
>   /\ Print("CRUD create object empty isEmpty", objectStore = EMPTY_STORE)
>      \* covered by TestObjectWithEvents
>   /\ objectStore' = Print("CRUD create object empty new", [x \in {objectId} |->
>         [class |-> ObjectClass,
>          id |-> objectId,
>          noHistory |-> noHistoryFunction,
>          mostRecent |-> NULL_FUNCTION,
>          events |-> NO_EVENTS] ])
>   /\ UNCHANGED enumeratedStore
> === end fragment
> 
> There are no parse errors. When I run a model that includes this module, I get the following error:
> 
> 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: In evaluation, the identifier objectStore is either undefined or not an operator.
> line 29, col 1 to line 36, col 37 of module Test2ObjectWithEvents
> The error occurred when TLC was evaluating the nested
> expressions at the following positions:
> 0. Line 38, column 33 to line 38, column 59 in Test2ObjectWithEvents
> 1. Line 191, column 32 to line 191, column 62 in ObjectWithEventsCrud
> 2. Line 188, column 6 to line 188, column 53 in ObjectWithEventsCrud
> 3. Line 188, column 6 to line 188, column 53 in ObjectWithEventsCrud
> 4. Line 163, column 6 to line 168, column 33 in ObjectWithEventsCrud
> 5. Line 163, column 6 to line 163, column 16 in ObjectWithEventsCrud
> 6. Line 29, column 1 to line 36, column 37 in Test2ObjectWithEvents
> 
> Stack Entry #3 points to the objectStore' expression above and #4 points to the "objectStore" string that's followed by the prime. This is consistent with the user output reported by the model:
> 
> "CRUD create object empty legal"  TRUE
> "CRUD create object empty id"  TRUE
> "CRUD create object empty isEmpty"  TRUE
> "CRUD create object empty legal"  TRUE
> "CRUD create object empty id"  TRUE
> "CRUD create object empty isEmpty"  TRUE
> 
> I've tried the following:
> 
> a. Change the variable name to something other than objectStore, throughout the specification. RESULT: no change - model evaluation stops at the same place.
> 
> b. Change the initialization of objectStore to avoid entering the createObjectInEmpty operation. RESULT: similar error involving objectStore', but at a different place in the module.
> 
> c. Change objectStore' to xxx' in the offending operation. RESULT: parse error.
> 
> d. Change objectStore' to objectStore in the offending line. RESULT: model runs to completion, but of course doesn't cover all the expected states; the line becomes a FALSE qualification that stops the state from changing, rather than a state change.
> 
> Note that the model reports detecting two errors (consistent with two sets of user output in the model), though the error stack reports only one.
> 
> An earlier version of this spec worked fine, so the editing has clearly triggered something bad. Anybody have any idea what's going on and (more importantly) how to fix it?

============= LATER =================
I still don't fully understand what's going on, but I now know how to trigger the problem. If I take the step

=== start fragment
addEvent1a == 
  /\ testState = "run" 
  /\ addEvent("o1","owner",3,4,[classification |-> "U",
      owner_id |-> "o1" ], EventDataToCurrent)
  /\ UNCHANGED testState
=== end fragment

and change it to

=== start fragment
addEvent1a == 
  /\ testState = "run" 
  /\ Print("some txt", addEvent("o1","owner",3,4,[classification |-> "U",
      owner_id |-> "o1" ], EventDataToCurrent) )
  /\ UNCHANGED testState
=== end fragment

then I get the error indicated above. It appears that putting a step inside a Print() all somehow messes with the toolkit's notion of the state variables. 

If this limitation is documented someplace, then I apologize for missing it. Otherwise IMO this is a bug, or at least an undocumented feature.