In the Linux labs, type the following command.
/home/robi/bin/valid
The best way to submit a VALID project is by having an own directory for each VALID project you create, i.e., for each exercise. VALID will put a lot of files into that directory. When you are done, just create an archive containing all files in the directory and submit it.
mkdir exercise1
(Create and edit your project)
cd exercise1
/home/robi/bin/valid
emacs README.txt
(Don't forget the README file!)
cd ..
(And now submit file
tar czf exercise1.tar.gz exercise1exercise1.tar.gz)
Click on the item you want to delete, and hit the
<Delete> key.
Double-click on the state name you want to change.
The Simulator only permits events that are possible in all automata of the model. Note that, if an event is listed in the event list of an automaton, it is disabled in all states that do not have an outgoing transition labelled with that event. If your event does not appear at all in the graph, it will never be enabled. This is marked by an open box in the Graph Editor's event list.
The above Machine1 automaton is faulty, because it never allows break2 or finish2 to happen.
Invoke Conflict Check from the Analysis menu.
You have to create another spec. Modifying the plant would mean to modify the physical system, which normally is not acceptable. But you can create a copy of the plant you want to change, and declare the copy to be an additional spec.
You are free to use any method you like.
Please make sure that I understand how you have obtained your solution.
If you use synthesis or similar features, please include all the original
automata in your submission, and explain in your README.txt
file which steps you took to construct the solution.
To be conflicting means that a marked state cannot
be reached from the end state of your trace. That it, it becomes impossible
to reach a configuration where all automata of your model are in their
marked states. If you are unlucky the trace is empty, in which case it is
impossible to reach any marked state at all.
Try the simulator and simulate until the end of the trace. Change mode to manual. Try to reach a marked state from here. You will find that it is not possible. Change the model so it becomes possible.
The simulator can tell you which automata are in their marked state and
which are not. Choose Show All from the Show menu and expand
the window. You must try to drive the model into a state where all automata
are in their marked states simultaneously.
Robi Malik,
Department of Computer Science, The University of Waikato;
