Models API

pyModelChecking provides implementations for directed graph and Kripke structures.

Graph API

It is used to define directed graphs and provides a method to compute the strogly connected components of a directed graph.

class pyModelChecking.graph.DiGraph(V=None, E=None)

Bases: object

A class to represent directed graphs.

A directed graph is a couple (V,E) where V is a set of vertices and E is a set of edges (i.e., pairs of vertices). If (s,d) in E, then s and d are said source and destination of (s,d).

add_edge(src, dst)

Add a new edge to a DiGraph

Parameters:

• src – the source node of the edge
• dst – the destination node of the edge

add_node(v)

Add a new node to a DiGraph

Parameters:

• self (DiGraph) – the DiGraph object
• v – a node

clone()

Clone a DiGraph

Returns:a clone of the DiGraph Return type:DiGraph

edges()

Return the edges of a DiGraph

Returns:a list of edges of the DiGraph Return type:list

edges_iter()

Return the edges of a DiGraph

Returns:the generator of edges of the DiGraph Return type:generator

get_reachable_set_from(nodes)

Compute the reachable set

Parameters:nodes (a container of nodes) – the set of nodes from which the reachability should be evaluated Returns:the set of the reachable nodes Return type:set

get_reversed_graph()

Build the reversed graph

Returns:the reversed graph Return type:DiGraph

get_subgraph(nodes)

Build the subgraph that respects a set of nodes

Returns:the subgraph that respects :param nodes: Return type:DiGraph

next(src)

Return the next of a node

Given a DiGraph \((V,E)\) and one of its node v, the next of \(v \in V\) is the set of all those nodes \(v'\) that are destination of some edge \((v,v') \in E\).

Returns:the set of nodes \(\{v' | (v,v') \in E\}\) Return type:set

nodes()

Return the nodes of a DiGraph

Returns:the list of the nodes of the DiGraph Return type:list

sources()

Return the sources of a DiGraph.

The sources of a DiGraph G are the nodes that are sources of some edges in G itself.

Returns:a generator of all the nodes that are sources of some edges Return type:generator

pyModelChecking.graph.compute_SCCs(G)

Compute the strongly connected components of a DiGraph

This method implements a non-recursive version of the Nuutila and Soisalon-Soinen’s algorithm ([ns94]) to compute the strongly connected components of a DiGraph.

[ns94]

E. Nuutila and E. Soisalon-Soinen. “On finding the strongly connected components in a directed graph.”, Information Processing Letters 49(1): 9-14, (1994)

Parameters:G (DiGraph) – the DiGraph object Returns:a generator of the sets of nodes of the strongly connected components of the DiGraph Return type:generator

Kripke API

It is used to define Kripke structures.

class pyModelChecking.kripke.Kripke(S=None, S0=None, R=None, L=None)

Bases: pyModelChecking.graph.DiGraph

A class to represent Kripke structures.

A Kripke structure is a directed graph equipped with a set of initial nodes, S0, and a labelling function that maps each node into the set of atomic propositions that hold in the node itself. The nodes of Kripke structure are called states.

clone()

Clone a Kripke structure

Returns:a clone of the current Kripke structure Return type:Kripke

get_fair_states(F)

Return a set of states from which leaves a fair path.

Parameters:F (a container) – a container of fairness constraints Returns:the set of states from which leaves a fair path Return type:set

get_substructure(V)

Return the sub-structure that respects a set of states

The sub-structure of a Kripke structure \((V',E',L')\) that respects a set of states \(V\) is the Kripke structure \((V,E,L)\) where \(E=E'\cap(V \times V)\) and \(L(v)=L'(v)\) for all \(s \in V\).

Parameters:V (set) – a set of states Returns:the sub-structure that respects V Return type:Kripke

label_fair_states(F)

Label all the fair states by a new atomic proposition.

This method labels all the states from which a fair path exists by using a new atomic proposition that means “there exists a fair path from here”. The new label is returned.

Parameters:F (a container) – a container of fairness constraints Returns:a new label that means “there exists a fair path from here” Return type:str

labelling_function()

Return the labelling function

Returns:the labelling function Return type:dict

labels(state=None)

Get the atomic propositions

This method gets the atomic propositions labelling either a state or the whole structure.

Parameters:state – either a state of the Kripke structure or None Returns:the atomic propositions that label either a state, whenever a parameter state is passed, or at least one state of the Kripke structure, otherwise Return type:set

next(src)

Return the next of a state

Given a Kripke structure \(K=(S,S0,R,L)\) and one of its state \(s\), the next of \(s\) in \(K\) is the set of all those states that are destination of some edges whose source is \(s\) itself i.e., \(K.next(s)=\{s' | (s,s') \in R\}\).

Returns:the set of nodes \(\{s' | (s,s') \in R\}\) Return type:set

replace_labelling_function(L)

Replace the labelling function

Parameters:L (dict) – a new labelling function for this Kripke structure Returns:the former labelling function Return type:dict

states()

Return the states of a Kripke structure

Returns:the states of the Kripke structure Return type:set

transitions()

Return the edges of a Kripke structure

Returns:the set of edges of the Kripke structure Return type:set

transitions_iter()

Return an interator of the edges of a Kripke structure

Returns:an interator of the set of edges of the Kripke structure Return type:iterator