[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Modelling interactive systems (state machines)

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?