static void
AutomatonAssignNext(
LtlTableau_t * tableau,
LtlSet_t * toCover,
LtlSet_t * s
)
- toCover = { u: X(u) is in s }. In other words, for each formula
of the form X(u) in the set 's', add the subformula u into 'toCover'.
- Side Effects 'toCover' is changed.
- Defined in
ltlAutomaton.c
static void
AutomatonBuildCover_Aux(
LtlTableau_t * tableau,
LtlSet_t * pToCover,
LtlSet_t * pCurrent,
LtlSet_t * pCovered,
lsList Cover
)
- the cover is updated in the parameter 'lsList Cover'. This
function is used in AutomatonBuildCover() only.
- Defined in
ltlAutomaton.c
static lsList
AutomatonBuildCover(
LtlTableau_t * tableau,
LtlSet_t * ToCover
)
- The cover is "a list of sets", where the sets are product terms
and the list is in DNF form (union of all its product terms).
- Side Effects The result should be freed by the caller.
- Defined in
ltlAutomaton.c
static void
AutomatonComputeFair(
LtlTableau_t * tableau,
LtlSet_t * r,
vertex_t * vtx1
)
- Each until formula in the 'untilUnqiueTable' corresponds to
a fair set (a set of vertices in the automaton, represented by a hash
table. A vertex belongs to a fair set iff its cover set contains the until
formula.
- Defined in
ltlAutomaton.c
static int
AutomatonComputeInitState(
Ltl_Automaton_t * A
)
- If there exists such a state 'ns', "Init" is not necessary:
(1) ns is in Aut->Init
(2) there is a edge from ns to every state in Aut->Init (including itself)
In another word, ns is equivalent to "Init".
(3) there is no edge fron ns to states not in Aut->Init.
Return the index of the state 'ns' if exist, otherwise return -1.
- Defined in
ltlCompose.c
static int
AutomatonCountSelector(
Ltl_Automaton_t * A
)
- The automaton is nondeterministic, but the blif_mv file should
be deterministic. Selector (variable with random output) is used to make
the .table determinstic. We need to know how many outputs the Selector
should have. Here we take the maximum out-degree among all nodes as the
upper bound estimation.
- Defined in
ltlCompose.c
static int
AutomatonCreateFairList(
LtlTableau_t * tableau,
Ltl_Automaton_t * aut
)
- The fairness in the tableau is "a hash table (Until formula,
FairVerticesList)". The fairness in the automaton should be " a list of
hash tables" (each hash table corresponds to a fair set, and a vertex is
in the hash table iff it's in that fair set).
Return 0 iff there is an empty fairset (which means the language of the
automaton is empty no matter what); Return 1 otherwise.
- Defined in
ltlAutomaton.c
static void
AutomatonGetInputNames(
Ltl_Automaton_t * A,
array_t * InputNames,
array_t * Name2LabelIdx
)
- InputNames and Name2LabelIdx are two "array_t" provided by the
caller. InputNames will be filled by all the labels on the automaton nodes;
Each item of Name2LabelIdx is a "st_table" from a label to all the related
formulae in A->labelTable that contains the label.
- Defined in
ltlCompose.c
static lsList
AutomatonLabelGetCubes(
Ltl_Automaton_t * A,
LtlSet_t * compositeLabel,
Ntk_Network_t * network
)
- The composite label can any combination of !, + , *.
- Defined in
ltlCompose.c
static int
AutomatonPartitionIsClique(
graph_t * G,
st_table * set
)
- Return 1 if the given table forms a clique (for each state, there
are edges to all the states in the set).
- Defined in
ltlMinimize.c
static st_table *
AutomatonPartitionLabelGLB(
st_table * set,
array_t * Negate
)
- Find the Greatest Lower Bound of the labels of a set of states, and
Return a hash table of A state that satisfy this 'GLB'. Return null if the
hash table is empty.
- Side Effects The result should be freed by the caller.
- Defined in
ltlMinimize.c
static st_table *
AutomatonPartitionLabelLUB(
st_table * set,
array_t * Negate
)
- Find the Least Upper Bound of the labels of a set of states, and
Return a hash table of states that satisfy this 'LUB'. Return null if the
hash table is empty.
- Side Effects The result should be freed by the caller.
- Defined in
ltlMinimize.c
static int
AutomatonPfairEquivQfair(
Ltl_Automaton_t * A,
vertex_t * state,
vertex_t * otherstate
)
- Return 1 iff the following statement in the automaton holds:
For each fair set, both states are in it or none of them (unless they are
'dontcare' states)
- Defined in
ltlMinimize.c
static int
AutomatonPfairImplyQfair(
Ltl_Automaton_t * A,
vertex_t * state,
vertex_t * otherstate
)
- Return 1 iff the following statement in the automaton holds:
For each fair set, if 'state' is in it, 'otherstate' must also in it.
(unless they are 'dontcare' states)
- Defined in
ltlMinimize.c
static lsList
AutomatonPickInputCandidate(
graph_t * G,
vertex_t * vtx
)
- Return the input-compatible candidates.
- Side Effects Result should be freed by the caller.
- Defined in
ltlMinimize.c
static lsList
AutomatonPickOutputCandidate(
graph_t * G,
vertex_t * vtx
)
- Return the output-compatible candidates.
- Side Effects Result should be freed by the caller.
- Defined in
ltlMinimize.c
static st_table *
AutomatonQuotientVertexGetClass(
vertex_t * vtx
)
- Return the partition component (a st_table) associated with the
given vertex in the Quotient graph.
- Side Effects The result is owned by the node, and should NOT be freed.
- Defined in
ltlMinimize.c
static LtlSet_t *
AutomatonSetCreate(
LtlTableau_t * tableau,
Ctlsp_Formula_t * F
)
- Its size will be the total number of sub-formulae in the
tableau. Only the bit corresponding to the given formula is set.
- Side Effects The result should be freed by the caller.
- Defined in
ltlAutomaton.c
static st_table *
AutomatonVertexGetImg(
graph_t * G,
vertex_t * vtx
)
- Return the image of the given vertex in the hash table.
- Side Effects Result should be freed by the caller.
- Defined in
ltlMinimize.c
static st_table *
AutomatonVertexGetPreImg(
graph_t * G,
vertex_t * vtx
)
- Return the pre-image of the given vertex in the hash table.
- Side Effects Result should be freed by the caller.
- Defined in
ltlMinimize.c
static int
AutomatonVertexHasSelfLoop(
graph_t * G,
vertex_t * vtx
)
- Return 1 iff the given vertex has a self-loop.
- Defined in
ltlMinimize.c
static int
AutomatonVtxGetNodeIdx(
vertex_t * v
)
- Return the node index associated with the given vertex.
- Defined in
ltlMinimize.c
static void
AutomatonVtxLabelToBlifMv(
FILE * fp,
Ltl_Automaton_t * A,
vertex_t * vtx
)
- Assume that the label is a propositional formula with *, +, !.
*
* For Ctlsp_ID_c/Ctlsp_NOT_c:
* .table in1 n1_##_label$AUT
* !(RED) 1
* For Ctlsp_AND_c:
* .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
* 1 1 1
* For Ctlsp_OR_c:
* .table n1_#1_label$AUT n1_#2_label$AUT n1_##_label$AUT
* 1 - 1
* - 1 1
- Defined in
ltlCompose.c
static int
CommandLtl2Aut(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv
)
- Translate LTL formulae given in file into Buechi automata
- Defined in
ltl.c
static int
CommandLtlMc(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv
)
- First, the LTL formula is parsed and translated into a
Buechi automaton (minimization techniques can by applied during the process).
Then, the Buechi Automaton is translated into a Hrc_Node in a newly created
Hrc_Manager. flatten_hierarchy/static_order are used to obtain the automaton
Network. In this process the same mddManager (as that of the design network)
is used.
Now we need to compose the (M x A). We choose to append the automaton network
to the design network. Partition is updated (or regenerated) for the composed
network.
A new FSM is created and the fairness are loaded in it. The fairness
constraints comes from both the design network and the automaton network.
Finally we use Mc_FsmCheckLanguageEmptiness() to do the language emptiness
checking. "Strength Reduction Technique" -- using different decision
procedures for strong, weak, and terminal automaon -- is used.
After the model check, we free everything we created in this command:
partition for (MxA), the new FSM, newly-created network nodes, the
automaton network as well as the automaton Hrc_Manager.
If necessary, the result mdd (which is the bad state -- a state that leads
to a fair path) can be saved. (for example, in the CTL* model checker).
- Defined in
ltl.c
static int
Contradiction(
LtlTableau_t * tableau,
int index,
LtlSet_t * ToCover,
LtlSet_t * Current,
LtlSet_t * Covered
)
- The formula is represented by its index in the abTable
- Defined in
ltlAutomaton.c
static lsList
GetCubes_Aux(
Ltl_Automaton_t * A,
int index
)
- The formula A->tableau->labelTable[index
- Defined in
ltlCompose.c
static int
HasToBeStored(
LtlTableau_t * tableau,
int index
)
- The formula is represented by its index in the abTable
- Defined in
ltlAutomaton.c
static void
HashNextFormulae(
LtlTableau_t * tableau,
Ctlsp_Formula_t * F
)
- Construct the 'X F' from the given 'F', and hash it.
- Defined in
ltlTableau.c
Ltl_Automaton_t *
LtlAutomatonGeneration(
LtlTableau_t * tableau
)
- Before calling this function, 'tableau' should contains:
1) LTL Formula (NNF) and its negation in a DAG (or UniqueTable)
2) alpha-beta Table (tableau-rule expansion of each sub-formulae )
3) Until formulae list.
- Side Effects The returned automaton should be freed by the caller.
- Defined in
ltlAutomaton.c
int
LtlAutomatonSetIsFair(
LtlTableau_t * tableau,
LtlSet_t * r
)
- It is used in Boolean minimization. It might prevent
over-simplification.
- Defined in
ltlAutomaton.c
LtlSet_t *
LtlAutomatonVertexGetLabels(
vertex_t * vtx
)
- Return the automaton node label set associated with the vertex.
- Side Effects The result is owned by the node, and should not be freed.
- Defined in
ltlMinimize.c
lsList
LtlCoverCofactor(
lsList Cover,
LtlSet_t * c,
array_t * Negate
)
- We need the Negate method for each item in the set.
- Side Effects The result need to be freed by the caller. The input is left
unchanged.
- Defined in
ltlSet.c
lsList
LtlCoverCompleteSum(
lsList Cover,
array_t * Negate
)
- The cover is represented by a list of sets (product terms).
- Side Effects The result should be freed by the caller. The given cover is
NOT changed.
- Defined in
ltlSet.c
LtlSet_t *
LtlCoverGetSuperCube(
lsList Cover,
array_t * Negate
)
- Return the supercube of a cover.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
int
LtlCoverIsImpliedBy(
lsList Cover,
LtlSet_t * term,
array_t * Negate
)
- Return 1 if the given cover is implied BY the set.
- Defined in
ltlSet.c
int
LtlCoverIsTautology(
lsList Cover,
array_t * Negate
)
- The test is not fast: the compute sum of the cover should be
computed.
- Defined in
ltlSet.c
lsList
LtlCoverPrimeAndIrredundant(
LtlTableau_t * tableau,
lsList Cover,
array_t * Negate
)
- First, compute a prime and irredundant version of the Cover;
Then try to drop each item iff it is implied by the remaining items.
Notice: there might be a bug in the algorithm. Need to be fixed.
Need to talke to Fabio/Roderick
- Defined in
ltlSet.c
void
LtlCoverPrintIndex(
int length,
lsList cover
)
- Print the cover as a set of index.
- Defined in
ltlSet.c
void
LtlFsmLoadFairness(
Fsm_Fsm_t * compFsm,
Fsm_Fairness_t * designFairness,
int NumberOfFairSets,
int * AutomatonStrength
)
- The fairness constraint comes from two places:
1) the fairness constraints on the model (designFairness);
2) the fairsets from the Buechi automaton (the LTL formula).
*AutomatonStrength is unchanged unless there are external fairness and the
automaton is terminal (in which case the strength is assumed to be "1-weak".
- Side Effects *AutomatonStrength might be changed.
- Defined in
ltl.c
static boolean
LtlMcAtomicFormulaCheckSemantics(
Ctlsp_Formula_t * formula,
Ntk_Network_t * network,
boolean inputsAllowed
)
- Perform simple static semantic checks on formula.
- See Also
Ltl_FormulaStaticSemanticCheckOnNetwork
- Defined in
ltl.c
Ltl_Automaton_t *
LtlMcFormulaToAutomaton(
Ntk_Network_t * network,
Ctlsp_Formula_t * Formula,
LtlMcOption_t * options,
int checkSemantics
)
- State-of-the-art Optiomization/Minimization is used to shrink
the size of the automaton:
1) Rewriting the Formula (before translation)
2) Boolean Minimization (during translation)
3) Automaton Minimization (after translation)
- prune fair states
- simulation-based minimization (io/direct/reverse)
For more information, refer to: Fabio Somenzi and Roderick Bloem,"Efficient
Buechi Automaton from LTL Formula," CAV'00.
Before translation, the sementics of the formula is checked on the model.
In the case it fails, a NIL pointer will be returned.
- Side Effects The returned automaton should be freed by the caller.
- Defined in
ltl.c
LtlMcOption_t *
LtlMcOptionAlloc(
)
- Alloc Memory for LtlMcOption_t.
- Defined in
ltl.c
void
LtlMcOptionFree(
LtlMcOption_t * result
)
- Free LtlMcOption_t, and close the ltl formula file.
- Defined in
ltl.c
int
LtlPairCompare(
const char * key1,
const char * key2
)
- For two keys with the same content, they are equal.
- Defined in
ltlSet.c
void
LtlPairFree(
LtlPair_t * pair
)
- Free the LtlPair_t data struture.
- Defined in
ltlSet.c
int
LtlPairHash(
char * key,
int modulus
)
- The key is based on the content. Thus two pair with the same
content (not necessarily the same pointer) have the same hash key.
- Defined in
ltlSet.c
LtlPair_t *
LtlPairNew(
char * First,
char * Second
)
- Allocate the data struture for 'pair'.
- Defined in
ltlSet.c
void
LtlPairPrint(
LtlPair_t * pair
)
- Print the pair as index pair.
- Defined in
ltlSet.c
void
LtlSetAssign(
LtlSet_t * to,
LtlSet_t * from
)
- Assign the content of 'from' to set 'to'.
- Side Effects set 'to' is changed.
- Defined in
ltlSet.c
int
LtlSetCardinality(
LtlSet_t * set
)
- Return how many bit is set to 1 in the given set.
- Defined in
ltlSet.c
void
LtlSetClearElt(
LtlSet_t * set,
int index
)
- Clear the bit indicated by 'index'.
- Side Effects The set is changed.
- Defined in
ltlSet.c
void
LtlSetClear(
LtlSet_t * set
)
- Clear all bits in the set.
- Side Effects The set is changed.
- Defined in
ltlSet.c
int
LtlSetCompareCardinality(
const void * p1,
const void * p2
)
- Return -1/0/+1 when 's1' has more/equal/less cardinality than
's2'.
- Defined in
ltlSet.c
LtlSet_t *
LtlSetConsensus(
LtlSet_t * first,
LtlSet_t * second,
array_t * Negate
)
- If the consesus does not exist, return a null pointer.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
LtlSet_t *
LtlSetCopy(
LtlSet_t * from
)
- Allocate the new set and copy the content of the given set.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
int
LtlSetEqual(
LtlSet_t * s1,
LtlSet_t * s2
)
- Return 1 if the two sets have the same content.
- Defined in
ltlSet.c
void
LtlSetFree(
LtlSet_t * set
)
- Free the data structure associated with 'set'.
- Defined in
ltlSet.c
int
LtlSetGetElt(
LtlSet_t * set,
int index
)
- Return the value of the bit indicated by 'index'.
- Side Effects The set is changed.
- Defined in
ltlSet.c
int
LtlSetInclude(
LtlSet_t * large,
LtlSet_t * small
)
- Return 1 iff 'large' includes 'small'.
- Defined in
ltlSet.c
int
LtlSetIsContradictory(
LtlSet_t * set,
array_t * Negate
)
- Return 1 iff the set contains both 'F' and '!F'.
- Defined in
ltlSet.c
int
LtlSetIsEmpty(
LtlSet_t * set
)
- Return 1 if the set is empty.
- Defined in
ltlSet.c
LtlSet_t *
LtlSetIsInList(
LtlSet_t * set,
lsList list
)
- Null will be return if there does not exist a match set.
- Defined in
ltlSet.c
mdd_t *
LtlSetModelCheckFormulae(
LtlSet_t * set,
array_t * labelTable,
Fsm_Fsm_t * fsm
)
- Return the supercube of a cover.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
LtlSet_t *
LtlSetNew(
int size
)
- Allocate the set data structure.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
void
LtlSetOR(
LtlSet_t * to,
LtlSet_t * from1,
LtlSet_t * from2
)
- Union the two sets 'from1' and 'from2', and assign to set 'to'.
- Side Effects set 'to' is changed.
- Defined in
ltlSet.c
void
LtlSetPrintIndex(
int length,
LtlSet_t * set
)
- The length of the set should be provided.
- Defined in
ltlSet.c
void
LtlSetPrint(
LtlTableau_t * tableau,
LtlSet_t * set
)
- Assume the set is based on the index table 'tableau->abTable'.
- Defined in
ltlSet.c
void
LtlSetSetElt(
LtlSet_t * set,
int index
)
- Set the bit indicated by 'index'.
- Side Effects The set is changed.
- Defined in
ltlSet.c
LtlSet_t *
LtlSetToLabelSet(
LtlTableau_t * tableau,
LtlSet_t * set
)
- The given set may contain all the 'elementary formulae'. Its
table and negation are 'tableau->abTable' and 'tableau->abTableNegate'.
The label set contain only the propositional formulae and their
negations. Its table and negation array are 'labelTable' and 'labelNegate'.
The above two table could have been the same, but we choose to implement
them differently: Since labelTable might be smaller than abTable, it will
make the boolean minimization based on it faster.
- Side Effects The result should be freed by the caller.
- Defined in
ltlSet.c
LtlTableau_t *
LtlTableauCreate(
)
- Allocate the data structure of tableau.
- Defined in
ltlTableau.c
void
LtlTableauFree(
LtlTableau_t * tableau
)
- Free the tableau data structure.
- See Also
LtlTableauGenerateTableau
- Defined in
ltlTableau.c
LtlTableau_t *
LtlTableauGenerateTableau(
Ctlsp_Formula_t * formula
)
- Generate the 'Tableau' sturcture for the LTL->AUT problem.
It first computes the NNF of the input formula, then create the alpha/beta
entry table for both the input formula and its negation according the
tableau rules, and finally compute the list of 'Until formulae'.
- See Also
LtlTableauGenerateRules
- Defined in
ltlTableau.c
Ctlsp_Formula_t *
LtlTableauGetUniqueXFormula(
LtlTableau_t * tableau,
Ctlsp_Formula_t * F
)
- If there does not exist, create and hash it into the unique
table.
- Defined in
ltlTableau.c
void
LtlTableauPrint(
FILE * fp,
LtlTableau_t * tableau
)
- Print the content of the tableau.
- See Also
LtlTableauGenerateTableau
- Defined in
ltlTableau.c
void
Ltl_AutomatonAddFairStates(
Ltl_Automaton_t * A
)
- Mark trivial SCCs as Fair states
- Defined in
ltlMinimize.c
void
Ltl_AutomatonComputeSCC(
Ltl_Automaton_t * A,
int force
)
- Traverse the entire reachable graph of the automaton, and
put all the SCCs in a hash table.
If force=1, the existing partition (A->SCC) is freed and the new partition
is computed.
If force=0, the partition is computed only if A->SCC=null.
- Side Effects A->SCC is assigned the new partition.
- Defined in
ltlMinimize.c
Ltl_Automaton_t *
Ltl_AutomatonCreateQuotient(
Ltl_Automaton_t * A,
st_table * partition
)
- The Quotient graph is represented as an automaton Q:
Q->SCC : partition component TO vertex in Q graph hash table
Q->Init: initial vertices in Q graph
Q->Fair: only 1 FairSet in it, which contains the Q vertices corresponding
to the fair components
Q->G : The actual graph_t
Each Q vertex is associated with an automaton node:
node->index: the index # of the Q vertex
node->Class: the partition component associated with this vertex.
NOTICE: the Quotient graph is NOT a DAG, non-trivial SCCs have self-loops.
- Side Effects A->SCC is updated with the following information:
if (key) is a trivial SCC (obviously non-fair), (value)=2;
if (key) is a non-trivial non-fair SCC, (value) = 0;
if (key) is a fair SCC, (value)=1;
otherwise, (value)=1;
The result should be freed by the caller.
- Defined in
ltlMinimize.c
Ltl_Automaton_t *
Ltl_AutomatonCreate(
)
- Allocate the automaton data structure.
- Defined in
ltlAutomaton.c
void
Ltl_AutomatonFree(
gGeneric g
)
- Free the automaton data structure.
- Defined in
ltlAutomaton.c
Mc_AutStrength_t
Ltl_AutomatonGetStrength(
Ltl_Automaton_t * A
)
- 0 -terminal 1 -weak 2 -strong.
- Side Effects Compute the parition and quotient graph if not exist.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonIsWeak(
Ltl_Automaton_t * A
)
- The definition of WEAK: For each fair SCC in the automaton,
every fairset F contains all its states.
A special case: If there is no fairness constraint at all, it's WEAK.
- Side Effects Compute the SCCs and Quotient graph(A->SCC,A->Q) if not exist.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonMaximizeByDirectSimulation(
Ltl_Automaton_t * A,
int verbosity
)
- Compute direct-simulation relation, and minimize the automaton
according to the following two cases:
1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa)
2) Remove edges from their common predecessors to p if p is direct
simulated by q.
- Side Effects The automaton might be changed. if so, return 1.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonMinimizeByDirectSimulation(
Ltl_Automaton_t * A,
int verbosity
)
- Compute direct-simulation relation, and minimize the automaton
according to the following two cases:
1) Remove p if (p,q) is a Bi-simulation relation (Bis-aa)
2) Remove edges from their common predecessors to p if p is direct
simulated by q.
- Side Effects The automaton might be changed. if so, return 1.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonMinimizeByIOCompatible(
Ltl_Automaton_t * A,
int verbosity
)
- These minimizations are based on the structural information,
and are less effective than simulation-based techniques. They are used for
pre-processing since they are faster.Also, in some cases they go beyond what
simulation based minimization can do.
Here we consider 3 cases: Input Compatible, Output Compatible and Dominance.
- Side Effects The automaton might be changed. In that case return 1.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonMinimizeByPrune(
Ltl_Automaton_t * A,
int verbosity
)
- We consider the following cases concerning fair SCCs:
1. Remove redundant transitions from predecessors of universal states (a
state with TRUE label and a self-loop, and it belongs to all fair sets.)
2. Remove all states that can not reach any fair SCC
3. Remove duplicate fair set and Shrink the fair sets
- Side Effects The automaton might be changed, in which case return 1. Also,
the A->SCC and A->Q are RE-computed.
- Defined in
ltlMinimize.c
int
Ltl_AutomatonMinimizeByReverseSimulation(
Ltl_Automaton_t * A,
int verbosity
)
- Compute Reverse-Simulation relation, and minimize the automaton
according to the following 2 cases:
1) remove p if (p,q) is a Bi-Simulation relation
2) remove edges from p to their common sucessors if p is reverse simulated
by q.
- Side Effects The automaton might be changed. if so, return 1.
- Defined in
ltlMinimize.c
Ltl_AutomatonNode_t *
Ltl_AutomatonNodeCreate(
Ltl_Automaton_t * aut
)
- Allocate the automaton node data structure.
- Defined in
ltlAutomaton.c
void
Ltl_AutomatonNodeFree(
gGeneric g
)
- Free the automaton node data structure.
- Defined in
ltlAutomaton.c
void
Ltl_AutomatonNodePrint(
Ltl_Automaton_t * aut,
Ltl_AutomatonNode_t * node
)
- Print the automaton node.
- Defined in
ltlAutomaton.c
void
Ltl_AutomatonPrint(
Ltl_Automaton_t * aut,
int verbosity
)
- Print the automaton.
- Defined in
ltlAutomaton.c
int
Ltl_AutomatonToBlifMv(
FILE * fp,
Ntk_Network_t * network,
Ltl_Automaton_t * A
)
- The Hrc_Manager may or may not be provided. If not, the blifmv
file generated is not complete (all the inputs are assummed to be boolean).
Notice that the labels on each state are propositional subformulae, not
necessarily atomic propositions.
- Defined in
ltlCompose.c
void
Ltl_AutomatonToDot(
FILE * fp,
Ltl_Automaton_t * aut,
int level
)
- Translate the Automaton into Dot format.
- Defined in
ltlCompose.c
int
Ltl_AutomatonToSmv(
FILE * fp,
Ntk_Network_t * network,
Ltl_Automaton_t * A
)
- The Hrc_Manager may or may not be provided. If not, the blifmv
file generated is not complete (inputs are assummed to be boolean.
- Defined in
ltlCompose.c
int
Ltl_AutomatonToVerilog(
FILE * fp,
Ntk_Network_t * network,
Ltl_Automaton_t * A
)
- The Hrc_Manager may or may not be provided. If not, the verilog
file generated is not accurate (all the inputs are assummed to be boolean).
- Defined in
ltlCompose.c
int
Ltl_AutomatonVtxGetNodeIdx(
vertex_t * v
)
- Return the node index associated with the given vertex.
- Defined in
ltlMinimize.c
void
Ltl_End(
)
- Ends the Ltl package.
- See Also
Ltl_Init
- Defined in
ltl.c
boolean
Ltl_FormulaStaticSemanticCheckOnNetwork(
Ctlsp_Formula_t * formula,
Ntk_Network_t * network,
boolean inputsAllowed
)
- Perform static semantic check of ltl formula on network.
Specifically, given an atomic formula of the form LHS=RHS, check that the LHS
is the name of a latch/wire in the network, and that RHS is of appropriate
type (enum/integer) and is lies in the range of the latch/wire values. If LHS
is a wire, and inputsAllowed is false, check to see that the algebraic
support of the wire consists of only latches and constants.
- Defined in
ltl.c
void
Ltl_Init(
)
- Initializes the Ltl package.
- See Also
Ltl_End
- Defined in
ltl.c
Hrc_Manager_t *
Ltl_McAutomatonToNetwork(
Ntk_Network_t * designNetwork,
Ltl_Automaton_t * automaton,
int verbosity
)
- A new Hrc_Manager_t is created, in which the network will
be stored. The translation goes as the following:
1) translate the Buechi automaton into a temp file (in blifmv format);
2) read in the temp file (into the new hrcMgr) by default blifmv parser
3) flatten_hierarchy to get the network
- Side Effects The returned Hrc_Manager_t should be freed by the caller.
- Defined in
ltl.c
Ltl_Automaton_t *
Ltl_McFormulaToAutomaton(
Ntk_Network_t * network,
Ctlsp_Formula_t * Formula,
int options_algorithm,
int options_rewriting,
int options_prunefair,
int options_iocompatible,
int options_directsim,
int options_reversesim,
int options_directsimMaximize,
int options_verbosity,
int checkSemantics
)
- The wrapper of LtlMcFormulaToAutomaton.
- Side Effects The returned automaton should be freed by the caller.
- See Also
LtlMcFormulaToAutomaton
- Defined in
ltl.c
static LtlMcOption_t *
ParseLtlMcOptions(
int argc,
char ** argv
)
- Parse the user input for command "ltl_model_check."
- Defined in
ltl.c
static LtlMcOption_t *
ParseLtlTestOptions(
int argc,
char ** argv
)
- Parse the user input for command "ltl_to_aut".
- Defined in
ltl.c
static int
Redundant(
LtlTableau_t * tableau,
int index,
LtlSet_t * ToCover,
LtlSet_t * Current,
LtlSet_t * Covered
)
- The formula is represented by its index in the abTable
- Defined in
ltlAutomaton.c
static int
SI(
LtlTableau_t * tableau,
int index,
LtlSet_t * A
)
- Return 1 if the formula is implied. The formula is represented
by its index in the abTable
- Defined in
ltlAutomaton.c
static void
ShuffleMddIdsToTop(
mdd_manager * mddManager,
array_t * mddIdArray
)
- This function is called to move the automaton variables to the
top most. This is believed to be the best variable ordering for the composed
system (M x A). The variable corresponding to the first item in mddIdArray
will be the top most.
- Defined in
ltl.c
static st_table *
StTableAppend(
st_table * tbl1,
st_table * tbl2
)
- Append the tbl2 to tbl1 and return tbl1.
- Side Effects tbl1 is permenently changed.
- Defined in
ltlMinimize.c
static char *
StTableDelete(
st_table * tbl,
char * item
)
- If 'item' is in the hash table, Delete it and return the real key;
Otherwise, return 0.
- Side Effects 'item' will not be modified.
- Defined in
ltlMinimize.c
static int
StTableInclude(
st_table * large,
st_table * small,
st_table * dontcare
)
- Return 1 if 'larger' include every items in 'small' except those
also in 'dontcare'. Notice that 'dontcare' can be a null pointer.
- Defined in
ltlMinimize.c
static int
StTableIsDisjoint(
st_table * tbl1,
st_table * tbl2,
st_table * dontcare
)
- Return 1 if the two tables shares nothing except those items also
in 'dontcare'. Notice that 'dontcare' can be a null pointer.
- Defined in
ltlMinimize.c
static int
StTableIsEqual(
st_table * tbl1,
st_table * tbl2,
st_table * dontcare
)
- Return 1 if tbl1 and tbl2 have the same items except those also
in 'dontcare'. 'dontcare' can be a null pointer.
- Defined in
ltlMinimize.c
static int
StTableIsFair(
lsList A_Fair,
st_table * Class
)
- Return 1 if the given tables intersect every tables in the list.
- Defined in
ltlMinimize.c
static st_table *
StTableRestrict(
st_table * tbl1,
st_table * tbl2
)
- Remove from tbl1 all the items that are not in tbl2.
- Side Effects tbl1 is changed and returned.
- Defined in
ltlMinimize.c
static st_table *
StTableSubtract(
st_table * tbl1,
st_table * tbl2
)
- Remove from tbl1 all the items that are in tbl2.
- Side Effects tbl1 is changed and returned.
- Defined in
ltlMinimize.c
static char *
StringNormalize(
char * inputString
)
- = => ==
+ => ||
* => &&
. => _
< => _
> => _
- Side Effects The caller should free the result
- Defined in
ltlCompose.c
static void
TableauClearMarks(
LtlTableau_t * tableau
)
- Clear the marks of all the formula in the tableau.
- Defined in
ltlTableau.c
static void
TableauLoadUntilSubFormulae(
LtlTableau_t * tableau,
Ctlsp_Formula_t * F
)
- Put all the Until sub-formulae in a list.
- Defined in
ltlTableau.c
static int
TableauRules(
LtlTableau_t * tableau,
Ctlsp_Formula_t * F
)
- 1) assign each formula F an index and an entry;
2) build for each formula F a expansion ( {A0B0 ^ A0B1} + {A1B0 ^ A1B1} )
- Defined in
ltlTableau.c
static void
TimeOutHandle(
)
- This function is called when the process receives a signal of
type alarm. Since alarm is set with elapsed time, this function checks if the
CPU time corresponds to the timeout of the command. If not, it reprograms the
alarm to fire later and check if the CPU limit has been reached.
- Defined in
ltl.c
static void
VtxLabelToBlifMv_Aux(
FILE * fp,
Ltl_Automaton_t * A,
int node_idx,
int index,
st_table * CreatedSignals
)
- Assume that "i" is the index in the label table
- Defined in
ltlCompose.c