ltl.c

LTL model checking.

ltlAutomaton.c

Translate LTL formula to the Buechi Automaton.

ltlCompose.c

Write the Buechi automaton into a file.

ltlMinimize.c

Buechi automaton minimization.

ltlSet.c

Set/Pair/Cover Manipulation functions used in the ltl package.

ltlTableau.c

Expand the LTL Formula by applying the Tableau Rules.

ltlUtil.c

Utilities for LTL model checker

By: Chao Wang

Ltl_Init()

Initializes the Ltl package.

Ltl_End()

Ends the Ltl package.

Ltl_McFormulaToAutomaton()

Translate the LTL formula into a Buechi automaton.

Ltl_McAutomatonToNetwork()

Translate the Buechi automaton into a network.

Ltl_FormulaStaticSemanticCheckOnNetwork()

Perform static semantic check of ltl formula on network.

LtlMcFormulaToAutomaton()

Translate the LTL formula to a Buechi automaton.

LtlFsmLoadFairness()

Load the Fairness Constraint for the compFsm.

LtlMcOptionAlloc()

Alloc Memory for LtlMcOption_t.

LtlMcOptionFree()

Free LtlMcOption_t, and close the ltl formula file.

CommandLtlMc()

Check LTL formulae given in file are modeled by flattened network

CommandLtl2Aut()

Translate LTL formulae given in file into Buechi automata

ParseLtlMcOptions()

Parse the user input for command "ltl_model_check."

ParseLtlTestOptions()

Parse the user input for command "ltl_to_aut".

LtlMcAtomicFormulaCheckSemantics()

Perform simple static semantic checks on formula.

TimeOutHandle()

Handle function for timeout.

ShuffleMddIdsToTop()

Move the mdd variables to the top most.

By: Chao Wang

Ltl_AutomatonCreate()

Allocate the automaton data structure.

Ltl_AutomatonFree()

Free the automaton data structure.

Ltl_AutomatonNodeCreate()

Allocate the automaton node data structure.

Ltl_AutomatonNodeFree()

Free the automaton node data structure.

Ltl_AutomatonNodePrint()

Print the automaton node.

Ltl_AutomatonPrint()

Print the automaton.

LtlAutomatonGeneration()

Generate the Buechi automaton from the formula.

LtlAutomatonSetIsFair()

Return 1 if the given set belongs to a fair set.

HasToBeStored()

Return 1 iff the elementary formula need to be stored.

Contradiction()

Return 1 iff there is there is a contradition so far.

Redundant()

Return 1 iff the given formula is redundant.

SI()

Test if the given formula is synatically implied by the existing set (product term).

AutomatonComputeFair()

Put the node into the fairset if it contains a until formula.

AutomatonCreateFairList()

Convert the fair sets of the tableau into the fair set in the automaton.

AutomatonAssignNext()

Generate the next-formulae set.

AutomatonSetCreate()

Create the set representation of the given formula.

AutomatonBuildCover()

Build the cover for a given set 'toCover'.

AutomatonBuildCover_Aux()

Recursively construct the cover.

By: Chao Wang

Ltl_AutomatonToDot()

Translate the Automaton into Dot format.

Ltl_AutomatonToBlifMv()

Translate the automaton to a BlifMv file.

Ltl_AutomatonToVerilog()

Translate the automaton to Verilog file.

Ltl_AutomatonToSmv()

Translate the automaton to SMV file.

AutomatonGetInputNames()

Return a array of all the inputnames of the automaton.

AutomatonCountSelector()

Return the upper bound number of nondeterministic selectors.

AutomatonComputeInitState()

Determine if "Init" state is necessary.

AutomatonLabelGetCubes()

Given a composite label, return a list of label (each of which is a cube.

GetCubes_Aux()

Given a index in A->tableau->labelTable, return a list of label (each of which is a cube.

StringNormalize()

Given a string, do the following replacement.

AutomatonVtxLabelToBlifMv()

Create the "label" signal in blif_mv format and print out.

VtxLabelToBlifMv_Aux()

Create the "label" signal in blif_mv format and print out.

By: Chao Wang

Ltl_AutomatonMinimizeByIOCompatible()

Minimize the Automaton using I/O Compatiblility and Dominance.

Ltl_AutomatonMinimizeByDirectSimulation()

Minimize the Automaton using Direct Simulation.

Ltl_AutomatonAddFairStates()

Mark trivial SCCs as Fair states

Ltl_AutomatonMaximizeByDirectSimulation()

Maximize the Automaton using Direct Simulation.

Ltl_AutomatonMinimizeByReverseSimulation()

Minimize the Automaton using Reverse Simulation.

Ltl_AutomatonMinimizeByPrune()

Remove states that cannot reach any fair SCC and perform other simplifications (simplify fair sets).

Ltl_AutomatonComputeSCC()

Compute the SCCs of the Automaton.

Ltl_AutomatonIsWeak()

Return 1 if if the automaton is 'WEAK'

Ltl_AutomatonGetStrength()

Return the strength of the automaton.

Ltl_AutomatonCreateQuotient()

Return the Quotient graph for the given partition.

Ltl_AutomatonVtxGetNodeIdx()

Return the node index associated with the given vertex.

LtlAutomatonVertexGetLabels()

Return the automaton node label set associated with the vertex.

AutomatonPickInputCandidate()

Return the input-compatible candidates.

AutomatonPickOutputCandidate()

Return the output-compatible candidates.

AutomatonVertexGetPreImg()

Return the pre-image of the given vertex in the hash table.

AutomatonVertexGetImg()

Return the image of the given vertex in the hash table.

AutomatonVertexHasSelfLoop()

Return 1 iff the given vertex has a self-loop.

AutomatonPfairEquivQfair()

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)

AutomatonPfairImplyQfair()

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)

StTableDelete()

If 'item' is in the hash table, Delete it and return the real key; Otherwise, return 0.

StTableAppend()

Append the tbl2 to tbl1 and return tbl1.

StTableRestrict()

Remove from tbl1 all the items that are not in tbl2.

StTableSubtract()

Remove from tbl1 all the items that are in tbl2.

StTableIsEqual()

Return 1 if tbl1 and tbl2 have the same items except those also in 'dontcare'. 'dontcare' can be a null pointer.

StTableInclude()

Return 1 if 'larger' include every items in 'small' except those also in 'dontcare'. Notice that 'dontcare' can be a null pointer.

StTableIsDisjoint()

Return 1 if the two tables shares nothing except those items also in 'dontcare'. Notice that 'dontcare' can be a null pointer.

StTableIsFair()

Return 1 if the given tables intersect every tables in the list.

AutomatonPartitionIsClique()

Return 1 if the given table forms a clique (for each state, there are edges to all the states in the set).

AutomatonPartitionLabelLUB()

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.

AutomatonPartitionLabelGLB()

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.

AutomatonQuotientVertexGetClass()

Return the partition component (a st_table) associated with the given vertex in the Quotient graph.

AutomatonVtxGetNodeIdx()

Return the node index associated with the given vertex.

By: Chao Wang

LtlSetNew()

Allocate the set data structure.

LtlSetFree()

Free the data structure associated with 'set'.

LtlSetCopy()

Allocate the new set and copy the content of the given set.

LtlSetAssign()

Assign the content of 'from' to set 'to'.

LtlSetEqual()

Return 1 if the two sets have the same content.

LtlSetCardinality()

Return how many bit is set to 1 in the given set.

LtlSetCompareCardinality()

Return -1/0/+1 when 's1' has more/equal/less cardinality than 's2'.

LtlSetIsContradictory()

Return 1 iff the set contains both 'F' and '!F'.

LtlSetInclude()

Return 1 iff 'large' includes 'small'.

LtlSetOR()

Union the two sets 'from1' and 'from2', and assign to set 'to'.

LtlSetClear()

Clear all bits in the set.

LtlSetSetElt()

Set the bit indicated by 'index'.

LtlSetClearElt()

Clear the bit indicated by 'index'.

LtlSetGetElt()

Return the value of the bit indicated by 'index'.

LtlSetIsEmpty()

Return 1 if the set is empty.

LtlSetIsInList()

Return the set in the list that matches the given set.

LtlSetToLabelSet()

Transform the given set to the label set and return it.

LtlSetPrint()

Print all the 'elementary formulae' contained in the set.

LtlSetPrintIndex()

Print all index that are set in the set.

LtlPairNew()

Allocate the data struture for 'pair'.

LtlPairFree()

Free the LtlPair_t data struture.

LtlPairHash()

Return a hash key for the given pair.

LtlPairCompare()

Return -1/0/+1 when the key1 is greater/equal/less than key2.

LtlPairPrint()

Print the pair as index pair.

LtlCoverPrintIndex()

Print the cover as a set of index.

LtlCoverCompleteSum()

Return the 'Complete Sum' of the cover by iterated consensus.

LtlSetConsensus()

Return the consensus of two given set (product terms).

LtlCoverCofactor()

Return the cofactor of the cover with respect to the set.

LtlCoverIsTautology()

Return 1 if the given cover is tautology.

LtlCoverIsImpliedBy()

Return 1 if the given cover is implied BY the set.

LtlCoverPrimeAndIrredundant()

Boolean minimization of the given cover.

LtlCoverGetSuperCube()

Return the supercube of a cover.

LtlSetModelCheckFormulae()

Return the supercube of a cover.

By: Chao Wang

LtlTableauGenerateTableau()

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

LtlTableauCreate()

Allocate the data structure of tableau.

LtlTableauFree()

Free the tableau data structure.

LtlTableauPrint()

Print the content of the tableau.

LtlTableauGetUniqueXFormula()

Return the unique formula 'X F' in the tableu by giving 'F'.

TableauClearMarks()

Clear the marks of all the formula in the tableau.

TableauRules()

Fill out the Alpha-Beta entry table recursively.

HashNextFormulae()

Hash the formula 'X F' and its negation in the unique tableau.

TableauLoadUntilSubFormulae()

Put all the Until sub-formulae in a list.

By: Chao Wang