As generated by function ComputeStateTrans, an EFSM might have states where the execution CAN be instantaneous, i.e., where the program CAN terminate under some conditions, where under other conditions, there might be further successor states. Function AddSinkState adds a new state with a self-loop as single outgoing transitions such that this new sink state is reached by all the states of the EFSM under their instantC conditions.

ComputePathsForVCs is used to compute the paths reaching SCCs and the transitions inside SCCs which are both needed to set up verification conditions for the EFSM. The result is a pair (pathsToSCC,insdSCC) where pathsToSCC is a map where for each SCC index i pathsToSCC[i] is a set of paths leading from other SCCs or the initial state to that SCC. A path is thereby a pair (s{0},[(phi{0},s{1}),...,(phi{N},s{N+1})]). Similarly, insdSCC is a map where insdSCC[i] is the set of transitions that move inside SCC i, where a transition is a triple (s,phi,s').

ComputeStateTrans applies FrontTrans during a depth first traversal over the control flow graph (the EFSM) of a given Quartz module. The function also determines indices of the states as the number that was used during the state traversal. Moreover, as done by Tarjan's algorithm, it determines via the sccIndex the index of the root of the first state reached of each state's SCC. This way, it also enumerates the SCCs of the graph. The result is an array of NodeOfEFSM records.

EFSM2Dot writes an EFSM as computed by ComputeStateTrans to a dot-file for viewing the EFSM. Using the parameters writeStmt and writeTransfers, one can determine whether the statements are written in the nodes and whether the transfer actions are written in the nodes.

FrontTrans computes for a given Quartz statement stmt the first reaction by means of the SOS rules. It requires the depth of a reincarnation (number of loop nests), a renaming of local variables rho, the condition to start the execution (both control and dataflow) strt, and a condition prmt to indicate a weakly preempted start. If both strt and prmt are true, then we only compute the dataflow actions, since the statement is not entered, and only the surface actions have to be collected. In other words: strtDF:=strt triggers the dataflow, and strtCF:=strt&!prmt triggers the entering of the control flow. To implement the meaning of immediate suspend statements as done by the translation to guarded actions, we furthermore provide an argument lbl that should contain the currently active control flow labels. If the suspension condition should hold, guarded actions will be generated that hold it at the current labels, instead of entering the label of the immediate suspend (which will be done if lbl should be empty). The function finally computes a record of type FrontSOS.

Generate the verification conditions for an EFSM; it is assumed that the EFSM has no deadend states, i.e., all states have successor states under all conditions. One has to apply function AddSinkState to achieve this in general.

Parse invariants from a text file provided by the user. The result is a list of pairs (phi,invM) where phi is a safety property to be proved, and invM is a map that maps SCC indices to the invariants that are to be used for an induction proof for that SCC.

PrintVerifCond prints a verification condition to Console.out

QuartzTool is the function to be called from the web page; it expects the following key/value pairs:

• QuartzModule: should contain a Quartz module
• withCF:
• writeStmt:
• writeTransfers:

Function FrontTrans generates new labels for the suspend statements, since these are converted to immediate suspend statements. If the suspend statements occur in a loop body, this may end up in an infinite loop generating always new labels. To avoid this, we remember once made computations of suspend statements and return them with the already existing labels.

use the Quartz compiler to compile the given module to guarded actions and expand the abbreviations for the compilation context and the guarded actions for printing; the result are the predicates inst,insd,term and the guarded actions for srfcCntr,srfcData,depthCntr,depthData.

print the compilation results of function getCompilationResult in html

simpBool computes a DNF of a given boolean formula. It is used to simplify path conditions of the EFSM to also detect inconsistencies. Nevertheless, some inconsistent path conditions will remain since the overall problem of checking inconsistency is undecidable (and NP-complete for boolean data types).