utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

State labels in mucalc formulas #185

Open ningit opened 4 years ago

ningit commented 4 years ago

The current syntax of mucalc formulas allows checking state propositions { s = v } where s designates an entry of the state vector and v is an integer or string value. This patch lets s refer to state labels too.

When s is not the name of a state part, it is understood as a state label and eventually checked using the GBgetStateLabelLong function. Syntactic sugar { p } has been defined for writing Boolean state labels { p = 1 }.

The changes are:

I have tested it with some examples and it works, but perhaps I have missed something, like the reason it had not been done before.