4.1 Grundlagen

Die Ausführung eines Netzes wird im Hauptmenü unter <F> angeboten. Falls noch kein Netz eingelesen wurde, erfragt INA zunächst ein Netz und anschließend gegebenenfalls die Zeitinformationen. Als nächstes können Sie die Schreiboptionen ändern und so Transitions- bzw. Farbnamen ausgeben lassen. Danach wird ein Menü angezeigt, das die verfügbaren Funktionen auflistet:

<R>: Reset to the initial state            <B>: Back to the previous state
<W>: Write the actual marking to a file
<S>: Show the stubborn set used by the stubborn reduced reachability graph
<A>: All minimal stubborn sets to be shown           <Q>: Quit computation

Vor jedem Schaltvorgang wird dieses Menü nocheinmal in einer verkürzten Form ausgegeben:

<r>eset | <b>ack | <w>rite | <s>tubborn set | <a>ll stubborn sets | <q>uit