Hi,
I'm trying to use PlusCal (or TLA+) to model an interactive safety-critical system. The system behaviour can be captured as a state machine with transitions on the form of event_or_message[conditions]/{actions}. I've a simple solution to define a variable for every event I expect and then at every possible state, I check the status of this variable...not sure if this is even correct or not?? But then when I run this, the model generates all possible combinations of the defined events - e.g. <true, true, true>, <true, true, false>, etc. which is still fine.
The problem is that these variables (of the events) will not change during the traversal of the execution paths.
What I want to do is that at each state I would like to re-enumerate all possible values for all these events. I tried to use CHOOSE but every time it returns the same value
Another similar scenario I face as well is at random points, one of the monitoring devices fails (randomly, so I need to have the index of the failed device random as well). Again using variables will result in having one scenario with device#1 always fail, another scenario with device#2 always fail, and so on. How this could be modelled using PlusCal.TLA+??
Another related question: can I model these events in one variable (only one event is valid at a time) let's say current_event which will be assigned to one element of the events set at a time? I did try this but again it generate all possible execution paths with each path one possible event during the whole execution (which shouldn't be the case).
Could you please advise?
Regards,
Mohamed