libmc Package¶

Provides collection of tools for KV Model Checking.

libmc.asynchronousComposition(*lts, partialOrderReduction=None)[source]¶

Asynchronous composition of two or more LTS through interleaving (p84).

performs on-the-fly generation of reachable states
Partial Order Reduction can be applied by supplying a function partialOrderReduction, selecting the components to expand

Keyword Arguments:
Parameters:	lts (variable argument list(LTS*)) – list of LTS to interleave
	partialOrderReduction (optional) – function `f: list(index) -> list(index)` selecting the local components to expand

class libmc.BDD[source]¶

Bases: object

Binary Decision Diagram (p149).

idx¶: int – node index

sign¶: bool – the node’s sign

child¶: list(BDD, BDD) – the node’s else and then successors

Note

Operations are carried out using the logical connectives ~, |, & and ^.

classmethod false()[source]¶: Boolean constant False.

isConstant()[source]¶: Returns True for constant nodes.

toDot()[source]¶

Returns a graphical representation of the BDD (using Graphviz).

Returns:	dot language representation
Return type:	string

classmethod true()[source]¶: Boolean constant True.

class libmc.Boole(formula)[source]¶

Bases: object

Evaluate and convert propositional formulae given in the Boole format [1].

References

[1]

limboole

evaluate(assignment)[source]¶

Evaluate the formula using a given assignment to it’s variables.

Parameters:	assignment (dict) – dictionary mapping variable names to truth values

toAIG()[source]¶

Converts the formula to an AIG in the AIGER format.

Returns:	AIG representing the formula in the AIGER format
Return type:	string

toBDD()[source]¶

Converts the formula to a BDD.

Returns:	BDD representing the formula
Return type:	BDD

truthTable()[source]¶

Generates the formula’s truth table.

Returns:	pairs combining assignments to the resulting truth value
Return type:	list

Warning

Since every possible assignment has to be evaluated, it might take a while for larger formulae!

libmc.bfs(queue, successors, **kwargs)[source]¶

Generic breadth-first search.

while queue:
    current = dequeue(queue)

    for successor in successors(current):
        if not cached(successor):
            cache(successor)
            enqueue(successor)

    if quit is not None and quit(current): return

Perform BFS on any given problem by defining:

the search queue’s initial state
a function returning the successors to a given object
(optional) a function for enqueuing objects
(optional) a function for adding objects to the cache
(optional) a function checking if a given object has been cached already
(optional) a function for stopping the search

Parameters:

queue (list) – initial state of the search queue
successors (function) – function f: object -> list(object) returning the list of successors to a given object

Keyword Arguments:

enqueue (function) – a function f: object -> None adding objects to the search queue
cache (function) – a function f: object -> None adding a given object to the cache (requires cached)
cached (function) – a function f: object -> bool checking if a given object has been cached already (requires cache)
quit (function) – a function f: object -> bool returning True if the search should stop with the given object

libmc.dfs(stack, successors, **kwargs)[source]¶

Generic depth-first search.

while stack:
    current = dequeue(stack)

    for successor in successors(current):
        if not cached(successor):
            cache(successor)
            enqueue(successor)

    if quit is not None and quit(current): return

Perform DFS on any given problem by defining:

the search queue’s initial state
a function returning the successors to a given object
(optional) a function for enqueuing objects
(optional) a function for adding objects to the cache
(optional) a function checking if a given object has been cached already
(optional) a function for stopping the search

Parameters:

queue (list) – initial state of the search queue
successors (function) – function f: object -> list(object) returning the list of successors to a given object

Keyword Arguments:

enqueue (function) – a function f: object -> None adding objects to the search queue
cache (function) – a function f: object -> None adding a given object to the cache (requires cached)
cached (function) – a function f: object -> bool checking if a given object has been cached already (requires cache)
quit (function) – a function f: object -> bool returning True if the search should stop with the given object

class libmc.FA(S, I, Σ, T, F)[source]¶

Bases: libmc.lts.LTS

Finite Automaton (p18).

S¶: set of states

I¶: set of initial states I ⊆ S

Σ¶: input alphabet

T¶: transition relation T ⊆ SxΣxS

F¶: set of final states F ⊆ S

accepts(word)[source]¶

Test acceptance of a given word.

Parameters:	word (list) – the word to check
Returns:	True if the word is accepted by the automaton
Return type:	bool

bisimulates(other, τ=[])¶

Bisimulation of LTS (p43).

∀ s ∊ self.I, ∃ t ∊ other.I [ s ≈ t ]

Parameters:	other (LTS) – another LTS τ (optional) – set of unobservable internal events
Returns:	True if this LTS bisimulates the other
Return type:	bool

complement()[source]¶: Create complement automaton (p23).

conforms(other, full=False)[source]¶

Conformance test (p24).

L(self) ⊆ L(other)
L(self) ∩ L(other) = 0
self × C(P(other)) contains no reachable final state (implemented)

Parameters:

other (FA) – the other FA to conform to
full (bool - optional) – create full automaton if True, else only reachable states are included (default)

Returns:

a triple containing:

the result of the conformance test
the generated checker automaton self × C(P(other))
all traces from initial to final states

Return type:

(bool, FA, list)

isComplete()¶: Completeness (p21): True if LTS is complete.

isDeterministic()¶: Determinism (p21): True if LTS is deterministic.

minimize()[source]¶: Minimization of Deterministic Finite Automata (p44).

power(full=False)[source]¶

Create power automaton (p22).

Parameters:	full (bool - optional) – create full automaton if True, else only reachable states are included (default)

product(other, full=False)[source]¶

Create product automaton (p20).

Parameters:	other (FA) – another FA full (bool - optional) – create full automaton if True, else only reachable states are included (default)

simulates(other, τ=[])¶

Simulation of LTS (p39).

∀ s ∊ other.I, ∃ t ∊ self.I [ s ≤ t ]

Parameters:	other (LTS) – another LTS τ (optional) – set of unobservable internal events
Returns:	True if this LTS simulates the other
Return type:	bool

toDot(highlight=[])[source]¶

Return FA as Graphviz dot language string.

Parameters:	highlight (list of transition lists - optional) – highlight the given paths
Returns:	.dot file tweaked for dot2tex
Return type:	string

toTex(highlight=[])[source]¶

Return LTS as TikZ based LaTeX figure (tikzpicture).

Parameters:	highlight (list of transition lists - optional) – highlight the given paths
Returns:	.tex file (tikzpicture)
Return type:	string

Note

Requires manual positioning!

trace(target, sources=None)¶

Tries to compute all traces to the target state (DFS).

If no source states are given, the set of initial states is used.

Parameters:	target – target state sources (optional) – set of initial states
Returns:	all paths (list of transitions) to the target or an empty list if it is unreachable
Return type:	list

class libmc.LTS(S, I, Σ, T)[source]¶

Bases: object

Labelled Transition System (p31).

S¶: set of states

I¶: set of initial states I ⊆ S

Σ¶: input alphabet

T¶: transition relation T ⊆ SxΣxS

bisimulates(other, τ=[])[source]¶

Bisimulation of LTS (p43).

∀ s ∊ self.I, ∃ t ∊ other.I [ s ≈ t ]

Parameters:	other (LTS) – another LTS τ (optional) – set of unobservable internal events
Returns:	True if this LTS bisimulates the other
Return type:	bool

isComplete()[source]¶: Completeness (p21): True if LTS is complete.

isDeterministic()[source]¶: Determinism (p21): True if LTS is deterministic.

power(full=False)[source]¶

Create power automaton (p22).

Parameters:	full (bool - optional) – create full automaton if True, else only reachable states are included (default)

product(other, full=False)[source]¶

Create product automaton (p20).

Parameters:	other (LTS) – another LTS full (bool - optional) – create full automaton if True, else only reachable states are included (default)

simulates(other, τ=[])[source]¶

Simulation of LTS (p39).

∀ s ∊ other.I, ∃ t ∊ self.I [ s ≤ t ]

Parameters:	other (LTS) – another LTS τ (optional) – set of unobservable internal events
Returns:	True if this LTS simulates the other
Return type:	bool

toDot(highlight=[])[source]¶

Return LTS as Graphviz dot language string.

Parameters:	highlight (list of transition lists - optional) – highlight the given paths
Returns:	.dot file tweaked for dot2tex
Return type:	string

toTex(highlight=[])[source]¶

Return LTS as TikZ based LaTeX figure (tikzpicture).

Parameters:	highlight (list of transition lists - optional) – highlight the given paths
Returns:	.tex file (tikzpicture)
Return type:	string

Note

Requires manual positioning!

trace(target, sources=None)[source]¶

Tries to compute all traces to the target state (DFS).

If no source states are given, the set of initial states is used.

Parameters:	target – target state sources (optional) – set of initial states
Returns:	all paths (list of transitions) to the target or an empty list if it is unreachable
Return type:	list

libmc.maximumSimulation(A1, A2, R0, τ=[])[source]¶

Constructs the maximum simulation relation A1 ≲ A2 (p36).

To get the full maximum simulation between two LTS A1 and A2 build the union of all possible permutations:

fullSimulationRelation =
    maximumSimulation(A1, A1, set(product(A1.S, A1.S))) |
    maximumSimulation(A1, A2, set(product(A1.S, A2.S))) |
    maximumSimulation(A2, A1, set(product(A2.S, A1.S))) |
    maximumSimulation(A2, A2, set(product(A2.S, A2.S)))

Parameters:	A1 (LTS) – some LTS A2 (LTS) – another LTS R0 (set) – the starting relation, e.g. A1.SxA2.S τ (optional) – set of unobservable internal events
Returns:	A1 ≲ A2 ⊆ R0 - the maximum simulation relation
Return type:	set

libmc.maximumBisimulation(A1, A2, R0, τ=[])[source]¶

Constructs the maximum bisimulation relation A1 ≈ A2 (p43).

Can also be used to minimize a deterministic automaton by constructing the state equivalence relation using:

maximumBisimulation(A, A, (A.FxA.F)∪((A.S\A.F)x(A.S\A.F)))

To get the full maximum bisimulation between two LTS A1 and A2 build the union of all possible permutations:

fullSimulationRelation =
    maximumBisimulation(A1, A1, set(product(A1.S, A1.S))) |
    maximumBisimulation(A1, A2, set(product(A1.S, A2.S))) |
    maximumBisimulation(A2, A1, set(product(A2.S, A1.S))) |
    maximumBisimulation(A2, A2, set(product(A2.S, A2.S)))

Parameters:	A1 (LTS) – some LTS A2 (LTS) – another LTS R0 (set) – the starting relation, e.g. A1.SxA2.S τ (optional) – set of unobservable internal events
Returns:	A1 ≈ A2 ⊆ R0 - the maximum simulation relation
Return type:	set

libmc.tarjan(nodes, edges)[source]¶

Tarjan’s Algorithm (p110).

Find strongly connected components in a directed graph.

Parameters:	nodes (iterable) – set of nodes edges (iterable) – set of edges (pairs of nodes)
Returns:	set of strongly connected components (list of nodes)
Return type:	list