Files
State machine in xfig format
The state machine above is of the Hangar Motor Controller which you have already seen. There are two 'init' procs. Go through the first init proc. Then, code up the second init (a new scenario) which is described below.
The second scenario is as follows:
1. up button
2. motortimeout event, no speed event.
3. ten_sec_timeout event
4. stop event
Follow this sequence thru on the state diagram.
Second: With both models, try changing the queue sizes from 0 to 1 (chan event = [1] of {mtype} ...) and see if it runs differently. It should.
Run the above model and explain why it behaves as it does. This can be run with:
spin -i nondeter.pr
to see each nondeterministic choice,or in XSpin, select run/set simulation parms/interactive.
You can also play with the random number generator seed in the same panel or use the -n switch on the command line (spin -n234 nondeter.pr).