fts2promela(graph,
procname=None)
|
|
Convert (possibly labeled) state graph to Promela str.
Creates a process which can be simulated as an independent thread in
the SPIN model checker. If atomic propositions label states, then they
are exported as bit variables.
The state graph is exported to Promela using goto statements. Goto
statements avoid introducing additional states. Using structured
constructs (if, do) can create extra states in certain cases.
The structured program theorem ensures that avoiding goto statements
is always possible. But this yields an equivalent algorithm only, not an
equivalent unfolding of the program graph.
Therefore verified properties can be affected, especially if
intermediate states are introduced in one of multiple processes.
- Parameters:
graph - networkxprocname (str (default: system name)) - Promela process name (after proctype)
|