Improve TLC checker script to be more flexible #1612
Conversation
Signed-off-by: see-quick <[email protected]>
| q_inv | ||
| EOF | ||
| # Step 2: Fix init predicate issue using Perl (cross-platform solution) | ||
| perl -0777 -i -pe "s/(.*)'\s+:= (.*_self_stabilization_.*?initial)/\1 = \2/s" "$tla_file" || err_and_exit "Failed to edit $tla_file" |
There was a problem hiding this comment.
This part here is the trickiest to generalize. The EWD426 spec has this init:
/// Initialize all nodes with non-deterministic states
action init = all {
nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf()
system' = initial
}
which in TLA+ becomes:
ewd426_3_self_stabilization_three_state_init ==
(\E ewd426_3_self_stabilization_three_state_initial \in [(0
.. ewd426_3_self_stabilization_three_state_N)
-> (0 .. 2)]:
ewd426_3_self_stabilization_three_state_system'
:= ewd426_3_self_stabilization_three_state_initial)
Where self_stabilization_three_state is the name of the module that instantiates ewd426.
So this substitution here is very specific to ewd426, which also only has one state variable and therefore requires a single substitution.
It will probably be easier to fix this inside Quint: when compiling to --target=tlaplus, replace assignments inside init with equalities. This will be required for the TLC integration anyway, so it's a more permanent fix.
I feel like I should try and make that change on Quint now, as that fix in combination with this amazing script improvements can get us to a pretty decent TLC integration.
There was a problem hiding this comment.
Ok, I managed to do something: #1613
I rushed this a bit and I'm not yet sure it covers all cases. Will have to write some tests and all. We can then remove this part of the script 😄
There was a problem hiding this comment.
Ok, I managed to do something: #1613. I rushed this a bit and I'm not yet sure it covers all cases. Will have to write some tests and all. We can then remove this part of the script 😄
Sure, no rush, take your time :)).
Signed-off-by: see-quick <[email protected]>
There was a problem hiding this comment.
I pushed some changes to drop the perl substitution that is no longer needed after #1613 was merged, and moving the new general script to a general folder.
I hope to soon find some time to incorporate this into Quint so we can quint verify --backend=tlc or something like that. Thanks for your contribution!
This PR changes a bit of the script where the TLC checker is needed.
Usage:
Now, one could change the use parameters to provide a better experience.
CHANGELOG.mdfor any new functionality