This function computes a fair initial path of the associated Kripke structure of a generalized Buechi automaton. The computed path is represented by a pair (initPath, cyclePath) of paths where initPath is a path from an initial state s0 to some state sK, and cyclePath is then a path from sK to sK that traverses all fairness constraints.

Given a structure k represented by BDDs and sets of states startStates and endStates (all are BDDs), function ComputePath computes an array of non-empty state sets [|S0;...;Sn|] such that each state in S[i] has a transition to a state in S[i+1], S[n] is contained in endStates, and S[0] is contained in startStates. Each S[i] is a cube, i.e., some variables are given concrete truth values, while others are don't cares. Thus, one can use arbitrary truth values for the remaining truth values to complete a single path through the transition system. If argument withTrans is given, then the path consists of at least one transition (otherwise, we would just get a state if startStates and endstates would have a nonempty intersection).

This function expects a given existential generalized Buechi automaton auto of the form ExistsAuto(qVars,initCond,transRel,fairConstr,acpt) as generated by function LTL2GeneralBuechi. The function computes the associated Kripke structure of that automaton and will represent that structure by Bdds. To this end, the function also initializes the Bdd package accordingly. The fair states are all states of the associated Kripke structure that have path where all fairness constraints hold infinitely often. Having computed the fair states, the function also computes the conjunction of the initial states with these states and also computes the conjunction of the fair states with the transition relation. The computation of the fair states is based on a fixpoint definition of the fair states condition (see also EmLe85, EmLe86a, EmLe86b, EmLe87, CGMZ95, SoRB02, SeTV05).

Convert a given LTL formula to an equivalent LO1 formula. Note that the generated formula is not type-consistent with the Quartz semantics, since we are using boolean arrays as monadic predicates. Note further that the three variables (t0,t1,t2) are sufficient, where the formula is applied at time t0 whereas t1 and t2 are auxiliary variables.

Compute the existential predecessor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.

prove validity of LTL formulas via emptiness checking of equivalent Büchi automata dotexe should be the path to graphviz, showCounterexample a flag which decides to print counterexamples as svg graphics, and psi is the formula

Compute the existential successor states of the states represented by Bdd phi in the Kripke structure k as a Bdd.

This cgi-function is used to compute predecessor and successor states in a symbolic way by simply expanding the boolean quantifier into the disjunction/conjunction of the cofactors.

This function is called by the cgi-interface for the TemporalLogicProver.

Printing a fair path which is given as two BddAdr arrays which each element denotes a state which is given as a cube. For printing, we better adapt to the state transition conventions, i.e., not mentioned variables are false, and don't cares have to be fixed to any value (choose false).