encode an explicitly encoded automaton by boolean variables so that automata of type AutomatonExpl are converted to AutomatonSymb

encode an explicitly encoded automaton by boolean variables so that automata of type AutomatonExpl are converted to AutomatonSymb

encode an explicitly encoded deterministic automaton by boolean variables so that automata of type AutomatonExpl are converted to DetAutomatonSymb

 Write a graphviz file to output stream ostr for an explicit automaton.
 The function stateStr is used to generate a label for the state, and the
 function labelStr is used to generate a label for the transition. For
 instance, these functions may look as follows:

     let transStr (i,o) =
         match o with 
          | None -> string i
          | Some(o) -> (string i)+"/"+(string o)

     let stateStr1 i = "s"+(string i)

     let stateStr2 s = string s

 If the parameter "bundle" is true, then at most one transition between
 a state pair is drawn that contains then the bundled list of input/output
 pairs instead of single transitions for each input/output combination
 between the same states.

reduce acceptance F to FG by using a watchdog: states s are replaced by pairs (s,w) with a boolean value w that becomes true when an accepting state has been reached by one of its predecessor states

reduce acceptance F to GF

reduce acceptance FG to F by using a watchdog: states s are replaced by pairs (s,w) with a boolean value w that can become true when an accepting state has been reached

reduce acceptance FG to GF

reduce acceptance G to any other one is done by reducing the automaton to the safe states, i.e., intersecting the initial states and transitions with the safe states

reduce an automaton to states that are reachable with infinite paths

Write a graphviz file to output stream ostr for an semi-symbolic automaton. The function stateStr is used to generate a label for the state. If the given automaton has many transitions between some state pairs, you may first apply function BundleAutoSemi.

reduce an automaton to states that are reachable with infinite paths

Convert a symbolic automaton to an explicit automaton by enumerating all possible assignments of all variables and reducing the transition relation to the next state condition.

Convert a symbolic automaton to a semi-symbolic automaton by enumerating all possible assignments to the state variables and reducing the transition relation to the enabling condition between two states. If useLogicMin holds, the enabling condition is also minimized (and this way also checked for being satisfiable).

AutoSymb2AutoSemiWithReachableStates is the same function as AutoSymb2AutoSemi, but is given the set of reachable states which can be computed by ComputeSpecialStatesAutoSymb. The generated automaton is then reduced to the reachable states only and therefore often smaller.

Write a graphviz file to output stream ostr for a symbolic automaton. The function converts the given automaton to a semi-symbolic one and generates the graphviz file for it.

reduce acceptance F to FG by using a watchdog that uses the new state variable with index qIdx

reduce acceptance F to GF by using a watchdog that uses the new state variable with index qIdx

reduce acceptance FG to F by using a watchdog that uses the new state variable with index qIdx

reduce acceptance FG to GF by using a watchdog that uses the new state variable with index qIdx

reduce acceptance G to any other one is done by reducing the automaton to the safe states, i.e., intersecting the initial states and transitions with the safe states

reduce an automaton to states that are reachable with infinite paths

optimize a semi-symbolic automaton in that all transitions between a state pair are combined into a single transition whose enabling condition is the disjunction of the enabling conditions of the transitions. Note that this is already the case for the automaton generated by function AutoSymb2AutoSemi.

Given an existential omega automaton as generated by function LTL2Omega, the function initializes the Bdd and computes the initial accepting states by a fixpoint computation. 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, BlGS00, FFKV01, HKSV97, HTKB93, KePR98, RaBS00, WBHR01, WBHR06, SoRB02, SeTV05).

CheckEmptinessbyNuSMV checks the emptiness of a given symbolic automaton using NuSMV whose executable file must be provided by smvExe.

ComputeSpecialStatesAutoSymb computes the states of an automaton that are reachable and that have an infinite outgoing path. The procedure makes use of BDDs in that the transition relation is constructed with the variable ordering Xq1;...;XqN;q1;...;qN;a1;...;aM. The function returns a triple (stateVarIds,reachBdd,infBdd) with the set of indices of the state variables, and the BDDs which encode the reachable states and the states with infinite outgoing paths.

convert a deterministic automaton to a AutoSymb without changing the transition relation etc.

This function applies the Breakpoint construction to construct a deterministic automaton whose states are pairs of sets of states of the given automaton such that ((q,qf),a,(q',qf')) is a transition iff there were states s,s' in q and q', respectively with (s,a,s'), and qf is the subset of states of q where since the last breakpoint only accepting states could be used to reach these states.

This function computes a symbolic representation of a deterministic automaton for a given nondeterministic automaton using the breakpoint construction. The deterministic automaton is computed similarly to the one of SymbolicRabinScott, but adds additional state variables b[i] that denote if the corresponding states p[i] belongs to the breakpoint set.

This function applies the Rabin-Scott subset construction to construct a deterministic automaton whose states are sets of states of the given automaton such that (q,a,q') is a transition iff there were states s,s' in q and q', respectively with (s,a,s').

 This function computes a symbolic representation of a deterministic 
 automaton for a given nondeterministic automaton. The nondeterministic
 automaton is given by its state variables, its initial condition, its
 transition relation, its acceptance condition, and the explicitly 
 enumerated set of its reachable states in terms of minterms which are 
 sets of state variables that contain those state variables that have
 positive occurrences in the minterm, i.e. which hold on the state.
 The latter can be computed by function ComputeSpecialStatesAutoSymb. 
 The determinization function associates then each reachable state 
 (minterm, set of state variables) with a new state variable of the 
 deterministic automaton whose name starts with the prefix "qDet".
 This way, a minterm on the new state variables corresponds with a set
 of sets of states of the nondeterministic automaton, since a minterm on
 the new state variables corresponds with a set of new state variables
 which is therefore a set of set of minterms of the old state variables,
 i.e., a set of set of states of the nondeterministic automaton.
 Details on the construction are given in MoSL08. 
 Note that the transition equations are of the form 
         next(pi) <-> p1&phi[i,1] | ... | pN&phi[i,N]
 where phi[i,j] is the set of inputs that trigger a transition from state
 pj to state pi in the nondeterministic automaton. This corresponds with
 the existential successor computation where pi is added to a successor
 state if one state pj can reach pi with input phi[i,j].

Determinize a given liveness automaton using the breakpoint construction after a reduction to a FG automaton

Determinize a given co-Büchi automaton using the breakpoint construction

Determinize a given safety automaton using the subset construction

Determinize a given total liveness automaton using the subset construction

Determinize a given automaton using either the subset or the breakpoint construction with additionally required steps (like reducing the states to the safe states before the determinization of safety automata). The strings qDet and bDet are the prefixes of the state variables used for encoding the supersets and breakpoint sets (if needed), and qIdx is the index of a state variable required for AutoSymbF2FG in case a NDet-F automaton must be converted to a NDet-FG automaton.

EncodeByMinterms generates a mapping that assigns to each element in the given sequence item a minterm using variables varNames{i} with the minimal number of variables. If parameter addNext is true, then the BoolNext constructor is added to the variables in the minterms. The function returns the indices of the names of the used variables and the generated mapping.

Check the equivalence of two deterministic (!) automata on finite words. It is assumed that both automata have the same inputs.

This function compute for SR-, JK- and T-flipflops the control logic. These functions are stored in a map that maps next state variables to the control logic functions.

check whether the automaton is a Moore automaton, i.e., it is a Mealy automaton where outputs only depend on inputs

Minimize a given deterministic finite state automatton on finite words

MintermsOfBdd computes all minterms that satisfy a given BDD. These minterms are obtained by using function AllSat to compute the satisfying cubes that are then extended to minterms which are encoded as sets of sets of variables. To this end, the function is given also the set of BDD indices of the variables that may occur in the BDD.

Parse an explicit automaton from a string: Inputs and outputs can be arbitrary strings, and the states are a set of integers. Each one of the parts can be omitted and is then either the empty set or determined by the transition or given sets of states. The acceptance type must be one of

GF | FG | G | F

or will become

FIN

if omitted. An example for a Mealy automaton is:

      inputs a,b;
      outputs c,d;
      init  0,1;
      trans (0,a,c,1); (0,b,d,0); (1,a,d,1); (1,b,c,0);

 

and an example for an omega-automaton is as follows:

     init   0,1;
     trans  (0,a,c,1); (0,b,d,0); (1,a,d,1); (1,b,c,0);
     fair   0;
     fair   0,1;
     accept 1;
     acpTy FG;

 

The order must be inputs/outputs/init/transitions/fair...fair/accept.

print explicit automaton

print a html table for the given counterexample consisting of the initial path to a cycle of states; the state variables are explained by the elementary subformulas that they abbreviate as given by defMap which may be empty, or the result of TemporalLogic.ExplainStateVars

print a html table for the given counterexample consisting of the initial path to a cycle of states; the state variables are explained by the elementary subformulas that they abbreviate as given by defMap which may be empty, or the result of TemporalLogic.ExplainStateVars

print the equivalence relation of EquivalentFSA or MinimalFSA

print a symbolic omega-automaton in Latex

print a symbolic deterministic omega-automaton in Latex with an optional acceptance condition that replaces the one of the automaton

 This function computes the transition monoid of the given automaton. The
 transition monoid is defined as the set of transition relations that are
 at first determined for every input, and then by closing this initial 
 set of transition relation with the relation product. The obtained 
 transition relations define the transition monoid of the automaton where
 the operation of the monoid is the relation product.
   This function computes for a given automaton a tuple (allTransRels,
 operTable,assocTable,isAperiodic) were allTransRels is the
 set of all transition relations of the monoid paired with their periods,
 operTable is a map that maps two transition relations to their product,
 assocTable is a map that maps each transition relation to the set of
 words that induce it, and isAperiodic holds if the monoid is aperiodic.

This function computes the transition monoid of the given symbolic automaton, i.e., the set of transition relations that relate states that can be reached by reading the same word. The operation table computes the relation product of these relations which is a finite monoid since the relation product is associative. The function also computes the period of each transition relation and checks whether the monoid is aperiodic, i.e., whether the automaton can be expressed as a temporal logic formula.

This function computes a BDD that encodes the winning conditions for the given deterministic omega-automaton with input and output variables. It is assumed that the output variables can be defined by a Mealy or Moore automaton to satisfy the acceptance condition for all words on the input variables. Note that we have the following:

• \(\mathsf{MooreSafe}(i,o,p) = \nu x.(p \wedge \langle ?o!i\rangle x)\)
• \(\mathsf{MealySafe}(i,o,p) = \nu x.(p \wedge \langle !i?o\rangle x)\)
• \(\mathsf{MooreLive}(i,o,p) = \mu x.(p \vee \langle ?o!i\rangle x)\)
• \(\mathsf{MealyLive}(i,o,p) = \mu x.(p \vee \langle !i?o\rangle x)\)

where \(\langle ?o!i\rangle x\) for a state prediate x(q) is defined as follows (the two alternatives are equivalent for deterministic R(q,i,o,q')): \[ \langle ?o!i\rangle x(q) := ?o.!i.!q'. R(q,i,o,q') \to x(q') = ?o.!i.?q'. R(q,i,o,q') \wedge x(q') \] This also shows the following dualities:

• \(\neg\mathsf{MooreSafe}(i,o,p) = \mu x.(\neg p \vee \langle !o?i\rangle x) = \mathsf{MealyLive}(o,i,\neg p)\)
• \(\neg\mathsf{MealySafe}(i,o,p) = \mu x.(\neg p \vee \langle ?i!o\rangle x) = \mathsf{MooreLive}(o,i,\neg p)\)
• \(\neg\mathsf{MooreLive}(i,o,p) = \nu x.(\neg p \wedge \langle !o?i\rangle x) = \mathsf{MealySafe}(o,i,\neg p)\)
• \(\neg\mathsf{MealyLive}(i,o,p) = \nu x.(\neg p \wedge \langle ?i!o\rangle x) = \mathsf{MooreSafe}(o,i,\neg p)\)

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).

check whether the automaton is an acceptor, i.e., it has no outputs

check whether the automaton is deterministic, i.e., whether it has for all states and inputs exactly one transition

check whether the automaton is an acceptor on finite words

check whether the automaton is a Mealy automaton, i.e., it has neither fairness constraints nor accepting states, but it has outputs

check whether the automaton is a Moore automaton, i.e., it is a Mealy automaton where outputs only depend on inputs

check whether the automaton is an omega-automaton

check whether the automaton is totally defined (so that we can use the subset construction for determinizing NDetF automata)