API Reference

mctk.checking module

This Module contains functions for Explicit-State Model Checking CTL properties on the class KripkeStruct.

We plan to support Symbolic Model Checking and Bounded Model Checking in the future.

Examples

>>> from mctk import *
>>> ks_json = {
...     "Atoms": ["a", "b", "c", "d"],
...     "States": {
...         "s1": 0b1000,  # s1 has labels "a"
...         "s2": 0b1100,  # s2 has labels "a", "b"
...         "s3": 0b0110,  # s3 has labels "b", "c"
...         "s4": 0b0111,  # s4 has labels "b", "c", "d"
...         "s5": 0b0100,  # s5 has label "b"
...         "s6": 0b0010,  # s6 has label "c"
...         "s7": 0b0001,  # s7 has label "d"
...     },
...     "Starts": ["s1"],
...     "Trans": {
...         's1': ['s2'],
...         's2': ['s3', 's4'],
...         's3': ['s4'],
...         's4': ['s7'],
...         's5': ['s6'],
...         's6': ['s7', 's5'],
...         's7': ['s5'],
...     },
... }
>>> ks = KripkeStruct(ks_json)
>>> sat_states = SAT_atom(ks, "a")
>>> print(sat_states)
{'s1', 's2'}
>>> sat_states = AND(SAT_atom(ks, "b"), SAT_atom(ks, "c"))
>>> print(sat_states)
{'s3', 's4'}
>>> sat_states = EX(ks, SAT_atom(ks, "a"))
>>> print(sat_states)
{'s2'}
>>> sat_states = EU(ks, SAT_atom(ks, "a"), SAT_atom(ks, "b"))
>>> print(sat_states)
{'s1', 's2', 's3', 's4', 's5'}
>>> sat_states = EG(tmp_ks, SAT_atom(tmp_ks, "a"))
>>> print(sat_states)
set()

mctk.checking.AF(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the AF operator on a CTL property.

Return a set of states where the CTL formula “AF property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “AF property” is satisfied

mctk.checking.AG(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the AG operator on a CTL property.

Return a set of states where the CTL formula “AG property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “AG property” is satisfied

mctk.checking.AND(property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the AND operator on two CTL properties.

Return a set of states where the CTL formula “property1 AND property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “property1 AND property2” is satisfied

mctk.checking.AU(ks: KripkeStruct, property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the AU operator on two CTL properties.

Return a set of states where the CTL formula “A property1 U property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “A property1 U property2” is satisfied

mctk.checking.AX(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the AX operator on a CTL property.

Return a set of states where the CTL formula “AX property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “AX property” is satisfied

mctk.checking.EF(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the EF operator on a CTL property.

Return a set of states where the CTL formula “EF property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “EF property” is satisfied

mctk.checking.EG(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the EG operator on a CTL property.

Return a set of states where the CTL formula “EG property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where “EG property” is satisfied

mctk.checking.EU(ks: KripkeStruct, property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the EU operator on two CTL properties.

Return a set of states where the CTL formula “E property1 U property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “E property1 U property2” is satisfied

mctk.checking.EX(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the EX operator on a CTL property.

Return a set of states where the CTL formula “EX property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “EX property” is satisfied

mctk.checking.IFF(ks: KripkeStruct, property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the IFF operator on two CTL properties.

Return a set of states where the CTL formula “property1 IFF property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “property1 IFF property2” is satisfied

mctk.checking.IMPLIES(ks: KripkeStruct, property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the IMPLIES operator on two CTL properties.

Return a set of states where the CTL formula “property1 IMPLIES property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “property1 IMPLIES property2” is satisfied

mctk.checking.NOT(ks: KripkeStruct, property1: Set[str]) → Set[str][source]

Implement the NOT operator on a CTL property.

Return a set of states where the CTL formula “NOT property” is satisfied.

Parameters:

ks – a Kripke Structure
property – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “NOT property” is satisfied

mctk.checking.OR(property1: Set[str], property2: Set[str]) → Set[str][source]

Implement the OR operator on two CTL properties.

Return a set of states where the CTL formula “property1 OR property2” is satisfied.

Parameters:

ks – a Kripke Structure
property1 – a CTL property represented as a set of states that satisfy the property
property2 – a CTL property represented as a set of states that satisfy the property

Returns:

a set of states where the CTL formula “property1 OR property2” is satisfied

mctk.checking.SAT_atom(ks: KripkeStruct, atomic_property: str) → Set[str][source]

Evaluate an atomic propositional property on a Kripke Structure.

Return a set of states where the atomic propositional property is satisfied.

Parameters:

ks – a Kripke Structure
atomic_property – an Atomic Propositional Property represented as a string

Returns:

a set of states where the Atomic Propositional Property is satisfied

Raises:

KripkeStructError – if the Atomic Property is not in the Kripke Structure

mctk.models module

This Module contains a class KripkeStruct, which is a graph implementation of Kripke Structures.

We plan to support other Transition Systems as well in the future.

class mctk.models.KripkeStruct(model_json=None)[source]

Bases: object

Class that implements a Kripke Structure for Model Checking.

An instance of thie class can be created from a JSON file or from scratch. For more information about Kripke Structures, see: https://en.wikipedia.org/wiki/Kripke_structure_(model_checking).

_atoms

Atoms, can only be reset before any state is created

Type:: tuple

_atoms_set

Atoms, a duplicate of “_atoms”, only for efficiency

Type:: set

_states

States, Key is the state name, Value is the state label

Type:: _UniqueValueDict

_starts

Start States

Type:: set

_trans

Transitions, Key is the source state, Value is a set of target states

Type:: defaultdict

_trans_inverted

Inverted Transitions, Key is the target state, Value is a set of source states

Type:: defaultdict

add_state(state: str, label: List[str]) → None[source]

Add a State to the Kripke Structure.

The State Label is a list of strings, where each string is an Atom. For example, if the atom is (“a”, “b”, “c”), then the label can be [“a”], [“a”, “b”, “c”], or [].

Parameters:

state – a string representing the State Name
label – a list of strings representing the State Label

Raises:

KripkeStructError – if the State Name or State Label exists, can’t add again
KrinkeStructError – if the State Label contains a Non-Eixsting Atom, can’t add it

Note

The parameter “label” should be a list to stay compatible with the JSON format. However, internally, the field “_states” is stored as a dict[str, int] for efficiency.

add_states(states: Dict[str, List[str]]) → None[source]

Add multiple States to the Kripke Structure.

Parameters:: states – a dict, Key is the State Name, Value is the State Label
Raises:: KripkeStructError – if a State Name or a State Label exists, can’t add again

add_trans(trans: Dict[str, Set[str]]) → None[source]

Add multiple Transitions to the Kripke Structure.

Parameters:: trans – a dict, Key is the Source State Name, Value is a list of Target State Names
Raises:: KripkeStructError – if Source or Target State doesn’t exist, can’t add transition

Note

The parameter “trans” should be a dict whose value is a list, to stay compatible with the JSON format. However, internally, the field “_trans” is stored as a dict whose value is a set for efficiency. For more information about list v.s. set, see: https://stackoverflow.com/questions/2831212/python-sets-vs-lists

get_SCCs() → List[Set[str]][source]

Get all Strongly Connected Components (SCCs) in the Kripke Structure.

Returns:: a list of sets, where each set contains the State Names in a SCC

get_atoms() → Tuple[str][source]

Get Atoms of the Kripke Structure.

Returns:: a tuple of strings representing the Atoms

get_label_of_state(state: str) → Set[str][source]

Given a State Name, get the corresponding State Label.

For example, if atoms is (“a”, “b”, “c”, “d”), the State Name is “s1”, and the State Label is 0b1010, then get_label_of_state(“s1”) will return the set {“a”, “c”}.

Parameters:: state – a string representing the State Name
Returns:: a set of strings representing the State Label, instead of the binary form
Raises:: KripkeStructError – if the State Name doesn’t exist, can’t get the Label of it

get_starts() → Set[str][source]

Get Start States of the Kripke Structure.

Returns:: a set of strings representing the Start States

get_state_names() → Set[str][source]

Get just State Names of the Kripke Structure.

Returns:: a set of strings representing the State Names

get_states() → Dict[str, int][source]

Get States of the Kripke Structure.

Returns:: a dict, Key is the State Name, Value is the State Label

Note

The State Label is store in the binary representation, instead of the list of strings.

get_trans() → defaultdict[str, Set[str]][source]

Get Transitions of the Kripke Structure.

Returns:: a defaultdict, Key is the Source State Name, Value is a set of Target State Names

get_trans_inverted() → defaultdict[str, Set[str]][source]

Get Inverted Transitions of the Kripke Structure.

Returns:: a defaultdict, Key is the Target State Name, Value is a set of Source State Names

remove_state(state: str) → None[source]

Remove a State from the Kripke Structure.

Parameters:: state – a string representing the State Name
Raises:: KripkeStructError – if the State Name doesn’t exist, can’t remove it

remove_states(states: List[str]) → None[source]

Remove multiple States from the Kripke Structure.

Parameters:: states – a list of strings representing the State Names

remove_trans(trans: Dict[str, List[str]]) → None[source]

Remove multiple Transitions from the Kripke Structure.

Parameters:: trans – a dict, Key is the Source State Name, Value is a list of Target State Names
Raises:: KripkeStructError – if a Transition doesn’t exist, can’t remove it

Note

The parameter “trans” should be a dict whose value is a list for efficiency, since it will only be iterated once. However, internally, the field “_trans” is stored as a dict whose value is a set for efficiency.

reverse_all_trans() → None[source]

Reverse all Transitions in the Kripke Structure.

This funciton is destructive!!! It will NOT create a new copy of the current Kripke Structure, but will directly modify the current Kripke Structure.

set_atoms(atoms: List[str]) → None[source]

Set Atoms of the Kripke Structure.

Parameters:: atoms – a list of strings representing the Atoms
Raises:: KripkeStructError – if any state exists, can’t reset atoms

Note

The parameter “atoms” should be a list to stay compatible with the JSON format. However, internally, the field “_atoms” is stored as a tuple for efficiency.

set_label_of_state(state: str, label_set: Set[str]) → None[source]

Given an existing State Name, (re)set the State Label.

Parameters:

state – a string representing the State Name
label_set – a set of strings representing the State Label

Raises:

KripkeStructError – if the State Name doesn’t exist, can’t (re)set the State Label
KripkeStructError – if the Label has been assigned to a differnt State Name, can’t assign it

Note

The parameter “label_set” should be a set, NOT a list, for efficiency.

set_starts(starts: List[str]) → None[source]

Set Start States of the Kripke Structure.

Parameters:: starts – a set of strings representing the Start States
Raises:: KripkeStructError – if a state doesn’t exist, can’t set it as a Start State

Note

The parameter “starts” should be a list to stay compatible with the JSON format. However, internally, the field “_starts” is stored as a set for efficiency.

exception mctk.models.KripkeStructError[source]

Bases: Exception

Exceptions raised by methods related to class KripkeStruct.