pyModelChecking

https://pymodelchecking.readthedocs.io/en/latest/
Admin
pyModelChecking is a Python model checking package capable of representing Kripke structures,...
Tokens:52,027
Snippets:398
Trust Score:9.6
Update:1 week ago
Show doc for...
Tokens:
Raw
### Get states and transitions of a Kripke structure

Source: https://pymodelchecking.readthedocs.io/en/latest/using_models.html

Shows how to retrieve the sets of states and transitions from a Kripke structure.

```python
>>> K.states()

[0, 1, 2, 3]

>>> K.transitions()

[(0, 1), (0, 2), (1, 0), (2, 2), (3, 2)]
```

--------------------------------

### Get labels of Kripke states

Source: https://pymodelchecking.readthedocs.io/en/latest/using_models.html

Shows how to retrieve the labels of all states or a specific state.

```python
>>> K.labels()

set(['q', 'p'])

>>> K.labels(3)

set(['q'])
```

--------------------------------

### Get successors of a state in a Kripke structure

Source: https://pymodelchecking.readthedocs.io/en/latest/using_models.html

Demonstrates the next method to obtain the successors of a given state.

```python
>>> K.next(0)

set([1, 2])
```

--------------------------------

### pyModelChecking.PL.language.get_symbols

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

Function to get symbols from an alphabet. This is a module-level function.

```APIDOC
## Function: pyModelChecking.PL.language.get_symbols

### Description
Function to get symbols from an alphabet. This is a module-level function.

### Signature
`get_symbols(alphabet)`

### Parameters
- **alphabet** - Required - The alphabet from which to get symbols.
```

--------------------------------

### Kripke.__init__(S=None, S0=None, R=None, L=None)

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Initializes a new Kripke structure with optional states, initial states, edges, and labelling function. Validates that the edge relation is total and that the labelling function is a dictionary.

```APIDOC
## Kripke.__init__(S=None, S0=None, R=None, L=None)

### Description
Initializes a new Kripke structure with optional states, initial states, edges, and labelling function. Validates that the edge relation is total and that the labelling function is a dictionary.

### Parameters
- **S** (collection) - Optional - A collection of states.
- **S0** (collection) - Optional - A collection of initial states.
- **R** (collection) - Optional - A collection of edges.
- **L** (dict) - Optional - A labelling function mapping each state to a set of atomic propositions.

### Returns
None

### Raises
- **RuntimeError** - If R is not total or L is not a dictionary.
```

--------------------------------

### Create a Kripke structure

Source: https://pymodelchecking.readthedocs.io/en/latest/using_models.html

Constructs a Kripke structure with states, transitions, and a labelling function, then prints it.

```python
>>> from pyModelChecking import *
>>> K = Kripke(S=[0, 1, 3],
...            R=[(0, 2), (2, 2), (0, 1), (1, 0), (3, 2)],
...            L={1: ['p', 'q'], 2: ['p', 'q'], 3: ['q']})
>>> print(K)

(S=[0, 1, 2, 3],S0=set([]),R=[(0, 1), (0, 2), (1, 0), (2, 2), (3, 2)],L={0: set([]), 1: set(['q', 'p']), 2: set(['q', 'p']), 3: set(['q'])})
```

--------------------------------

### EX

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula E(X(psi)).

```APIDOC
## EX

### Description
A shortcut to build the CTL formula E(X(psi)).

### Method
`EX(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula E(X(psi)).

### Example
```python
formula = EX(p)
```
```

--------------------------------

### Kripke.labels(state=None)

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Gets the atomic propositions labelling either a specific state or the whole structure. If no state is given, returns the union of all labels.

```APIDOC
## Kripke.labels(state=None)

### Description
Gets the atomic propositions labelling either a specific state or the whole structure. If no state is given, returns the union of all labels.

### Parameters
- **state** (optional) - Optional - A state of the Kripke structure. If None, returns all atomic propositions in the structure.

### Returns
- **set** - The atomic propositions labelling the given state, or the union of all labels if state is None.

### Raises
- **RuntimeError** - If the given state is not a state of the Kripke structure.
```

--------------------------------

### PathQuantifier.__init__

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTLS/language.html

Initializes a path quantifier formula with a subformula.

```APIDOC
## PathQuantifier.__init__

### Description
Initializes a path quantifier formula with a subformula.

### Method
Constructor

### Parameters
- **phi** (Formula) - Required - The subformula to wrap.

### Example
```python
A(phi)
```
```

--------------------------------

### get_reachable_set_from

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/graph.html

Computes the set of nodes reachable from a given set of starting nodes in the DiGraph. Uses a breadth-first traversal to collect all reachable nodes.

```APIDOC
## get_reachable_set_from

### Description
Computes the set of nodes reachable from a given set of starting nodes in the DiGraph. Uses a breadth-first traversal to collect all reachable nodes.

### Method
Function

### Signature
`get_reachable_set_from(self, nodes)`

### Parameters
- **nodes** (container of nodes) - Required - The set of nodes from which the reachability should be evaluated.

### Returns
- **set** - The set of reachable nodes.

### Example
```python
G = DiGraph(V=[1,2,3], E=[(1,2),(2,3)])
reachable = G.get_reachable_set_from([1])
```
```

--------------------------------

### EX() (in module pyModelChecking.CTL.language)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

CTL formula constructor for 'exists next'.

```APIDOC
## EX() (in module pyModelChecking.CTL.language)

### Description
CTL formula constructor for 'exists next'.
```

--------------------------------

### EG

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula E(G(psi)).

```APIDOC
## EG

### Description
A shortcut to build the CTL formula E(G(psi)).

### Method
`EG(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula E(G(psi)).

### Example
```python
formula = EG(p)
```
```

--------------------------------

### clone()

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Creates a clone of the current Kripke structure.

```APIDOC
## clone()

### Description
Creates a clone of the current Kripke structure.

### Method
`clone()`

### Returns
- **rtype**: Kripke - a clone of the current Kripke structure
```

--------------------------------

### transitions()

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Returns the set of edges of the Kripke structure.

```APIDOC
## transitions()

### Description
Returns the set of edges of the Kripke structure.

### Method
`transitions()`

### Returns
- **rtype**: set - the set of edges of the Kripke structure
```

--------------------------------

### Model check CTL* formula on Kripke structure

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Creates a Kripke structure and model checks the formula psi, returning the set of states satisfying it. Also demonstrates fair model checking with a fairness constraint F=[6].

```python
>>> from pyModelChecking import Kripke
>>> K = Kripke(R=[(0, 1), (0, 2), (1, 4), (4, 1), (4, 2), (2, 0),
...               (3, 2), (3, 0), (3, 3), (6, 3), (2, 5), (5, 6)],
...            L={0: set(), 1: set(['Start', 'Error']), 2: set(['Close']),
...               3: set(['Close', 'Heat']),
...               4: set(['Start', 'Close', 'Error']),
...               5: set(['Start', 'Close']),
...               6: set(['Start', 'Close', 'Heat'])})
>>> modelcheck(K, psi)

set([0, 1, 2, 3, 4, 5, 6])

>>> modelcheck(K, psi, F=[6])

set([])

```

--------------------------------

### EF

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula E(F(psi)).

```APIDOC
## EF

### Description
A shortcut to build the CTL formula E(F(psi)).

### Method
`EF(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula E(F(psi)).

### Example
```python
formula = EF(p)
```
```

--------------------------------

### Model Check CTL* Formula

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows how to perform CTL* model checking and fair model checking on a Kripke structure.

```APIDOC
## Model Check CTL* Formula

### Description
Perform CTL* model checking and fair model checking on a Kripke structure.

### Usage
```python
from pyModelChecking import Kripke
from pyModelChecking.CTLS import modelcheck

K = Kripke(R=[(0, 1), (0, 2), (1, 4), (4, 1), (4, 2), (2, 0),
              (3, 2), (3, 0), (3, 3), (6, 3), (2, 5), (5, 6)],
           L={0: set(), 1: set(['Start', 'Error']), 2: set(['Close']),
              3: set(['Close', 'Heat']),
              4: set(['Start', 'Close', 'Error']),
              5: set(['Start', 'Close']),
              6: set(['Start', 'Close', 'Heat'])})

# Model check a CTL* formula object
result = modelcheck(K, psi)

# Fair model check with fairness constraint F=[6]
result_fair = modelcheck(K, psi, F=[6])
```

### Notes
- The function `modelcheck` can also accept a string representation of a CTL* formula.
- If a string is passed, you can either provide a parser object or let the function create one automatically.
- Analogous functionality is provided for CTL and LTL via `pyModelChecking.CTL` and `pyModelChecking.LTL`.
```

--------------------------------

### DiGraph.__init__(V=None, E=None)

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/graph.html

Initializes a new DiGraph with optional collections of nodes and edges. Raises RuntimeError if the edges collection is not a container of pairs of hashable objects.

```APIDOC
## DiGraph.__init__(V=None, E=None)

### Description
Initializes a new DiGraph with optional collections of nodes and edges. Raises RuntimeError if the edges collection is not a container of pairs of hashable objects.

### Parameters
- **V** (collection) - Optional - A collection of nodes.
- **E** (collection) - Optional - A collection of edges, each edge being a pair (source, destination).

### Exceptions
- **RuntimeError** - If E is not a container of pairs of hashable objects.
```

--------------------------------

### Define CTL* Formula

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows how to import the CTLS sub-module and define a CTL* formula using the provided classes.

```APIDOC
## Define CTL* Formula

### Description
Import the CTLS sub-module and define a CTL* formula using the provided classes.

### Usage
```python
from pyModelChecking.CTLS import *

phi = A(G(
        Imply(And(Not('Close'),
                  'Start'),
              A(Or(G(Not('Heat')),
                   F(Not('Error')))))
        ))
```

### Notes
- Path quantifiers A and E and temporal operators X, F, G, U, R are provided as classes.
- These classes wrap strings and Boolean values as objects of `pyModelChecking.CTLS.language.AtomicProposition` and `pyModelChecking.CTLS.language.Bool`.
```

--------------------------------

### AX

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula A(X(psi)).

```APIDOC
## AX

### Description
A shortcut to build the CTL formula A(X(psi)).

### Method
`AX(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula A(X(psi)).

### Example
```python
formula = AX(p)
```
```

--------------------------------

### AF

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula A(F(psi)).

```APIDOC
## AF

### Description
A shortcut to build the CTL formula A(F(psi)).

### Method
`AF(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula A(F(psi)).

### Example
```python
formula = AF(p)
```
```

--------------------------------

### Build formulas with And, Imply, Or, Not

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Demonstrates constructing formulas using the And, Imply, Or, and Not classes. Shows automatic wrapping of strings and Boolean values, and that passing too many arguments raises a TypeError.

```python
>>> And('p', true)

(p and true)

>>> And('p', true, 'p')

(p and true and p)

>>> f = Imply('q','p')
>>> And('p', f, Imply(Not(f), Or('q','s', f)))

(p and (q --> p) and (not (q --> p) --> (q or s or (q --> p))))

>>> Imply('p', 'q', 'p')
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: __init__() takes exactly 3 arguments (4 given)

```

--------------------------------

### Kripke

Source: https://pymodelchecking.readthedocs.io/en/latest/models_API.html

Documentation for the Kripke class in the pyModelChecking.kripke module, including its constructor and all public methods.

```APIDOC
## Kripke

### Description
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.

### Constructor
`Kripke(S=None, S0=None, R=None, L=None)`

### Methods

#### clone()
Returns a clone of the current Kripke structure.

**Returns:** a clone of the current Kripke structure (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 (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′∩(V×V) and L(v)=L′(v) for all s∈V.

**Parameters:**
- **V** (set) – a set of states

**Returns:** the sub-structure that respects V (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” (str)

#### labelling_function()
Return the labelling function.

**Returns:** the labelling function (dict)

#### labels(state=None)
Get 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 (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′)∈R}.

**Returns:** the set of nodes {s′|(s,s′)∈R} (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 (dict)

#### states()
Return the states of a Kripke structure.

**Returns:** the states of the Kripke structure (set)

#### transitions()
Return the edges of a Kripke structure.

**Returns:** the set of edges of the Kripke structure (set)

#### transitions_iter()
Return an iterator of the edges of a Kripke structure.

**Returns:** an iterator of the set of edges of the Kripke structure (iterator)
```

--------------------------------

### EG(psi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build E(G(ψ)). Returns the formula E(G(ψ)) where ψ is the method parameter.

```APIDOC
## EG(psi)

### Description
A shortcut to build E(G(ψ)). Returns the formula E(G(ψ)) where ψ is the method parameter.

### Method
EG

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula E(G(ψ)).
```

--------------------------------

### Parse propositional formulas with Parser

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows how to use the Parser class to read formulas from strings and convert them into Formula objects.

```python
>>> p = Parser()

>>> p('p and true')

(p and true)

>>> p('(~p and q) --> ((q | p))')

((not p and q) --> (q or p))

```

--------------------------------

### model_checking(kripke, formula, parser=None, F=None)

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/model_checking.html

Model checks a CTL formula against a Kripke structure. Returns a list of states satisfying the formula. Supports string formulas with a parser and fair states.

```APIDOC
## model_checking(kripke, formula, parser=None, F=None)

### Description
Model checks a CTL formula against a Kripke structure. Returns a list of states satisfying the formula. Supports string formulas with a parser and fair states.

### Parameters
- **kripke** (Kripke) - Required - A Kripke structure.
- **formula** (CTL.Formula or str) - Required - The formula to model check. Can be a CTL formula or a string representing a CTL formula.
- **parser** (CTL.Parser) - Optional - A parser to parse a string into a CTL.Formula.
- **F** (Container) - Optional - A list of fair states.

### Returns
- **list** - A list of the Kripke structure states that satisfy the formula.

### Raises
- **TypeError** - If the formula is not a CTL state formula or the kripke is not a Kripke structure.
```

--------------------------------

### __str__()

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Returns a string representation of the Kripke structure.

```APIDOC
## __str__()

### Description
Returns a string that represents a Kripke structure.

### Method
`__str__()`

### Returns
- **rtype**: str - a string that represents the Kripke
```

--------------------------------

### EU(psi, phi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build E(U(ψ,ϕ)). Returns the formula E(U(ψ,ϕ)) where ψ and ϕ are the method parameters.

```APIDOC
## EU(psi, phi)

### Description
A shortcut to build E(U(ψ,ϕ)). Returns the formula E(U(ψ,ϕ)) where ψ and ϕ are the method parameters.

### Method
EU

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.
- **phi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula E(U(ψ,ϕ)).
```

--------------------------------

### Operator Shortcuts: ~, &, |

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Use the overwritten operators ~, &, and | as shortcuts to Not, And, and Or constructors.

```APIDOC
## Operator Shortcuts: ~, &, |

### Description
Use the overwritten operators ~, &, and | as shortcuts to Not, And, and Or constructors. At least one operand must be a Formula object.

### Usage
```python
AtomicProposition('p') & True
True & AtomicProposition('p')
f = 'p' & Bool(True)
~('p' & Bool(True)) | And(~f,'b')
```

### Parameters
- **left** (Formula or str or bool) - Required - Left operand.
- **right** (Formula or str or bool) - Required - Right operand.

### Returns
- **Formula** - The resulting formula object.
```

--------------------------------

### AF(psi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build A(F(ψ)). Returns the formula A(F(ψ)) where ψ is the method parameter.

```APIDOC
## AF(psi)

### Description
A shortcut to build A(F(ψ)). Returns the formula A(F(ψ)) where ψ is the method parameter.

### Method
AF

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula A(F(ψ)).
```

--------------------------------

### Kripke.states()

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Returns the set of states in the Kripke structure.

```APIDOC
## Kripke.states()

### Description
Returns the set of states in the Kripke structure.

### Returns
- **set** - The states of the Kripke structure.
```

--------------------------------

### AG(psi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build A(G(ψ)). Returns the formula A(G(ψ)) where ψ is the method parameter.

```APIDOC
## AG(psi)

### Description
A shortcut to build A(G(ψ)). Returns the formula A(G(ψ)) where ψ is the method parameter.

### Method
AG

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula A(G(ψ)).
```

--------------------------------

### Create atomic propositions and Boolean values

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows how to create atomic propositions and Boolean values using the pyModelChecking.PL sub-module. The output displays the formula representation.

```python
>>> from pyModelChecking.PL import *
>>> AtomicProposition('p')

p

>>> Bool(True)

true

```

--------------------------------

### ER() (in module pyModelChecking.CTL.language)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

CTL formula constructor for 'exists release'.

```APIDOC
## ER() (in module pyModelChecking.CTL.language)

### Description
CTL formula constructor for 'exists release'.
```

--------------------------------

### AG

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula A(G(psi)).

```APIDOC
## AG

### Description
A shortcut to build the CTL formula A(G(psi)).

### Method
`AG(psi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula A(G(psi)).

### Example
```python
formula = AG(p)
```
```

--------------------------------

### Use operator shortcuts &, |, ~

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows using the overloaded operators &, |, and ~ as shortcuts for And, Or, and Not constructors. At least one operand must be a Formula object; otherwise a TypeError occurs.

```python
>>> AtomicProposition('p') & True

(p and true)

>>> True & AtomicProposition('p')

(true and p)

>>> f = 'p' & Bool(True)
>>> f

(p and true)

>>> True & 'p' & Bool(True)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: unsupported operand type(s) for &: 'bool' and 'str'

>>> 'p' & Bool(True) & 'p'

((p and true) and p)

>>> ~('p' & Bool(True)) | And(~f,'b')

(not (p and true) or (not (p and true) and b))

```

--------------------------------

### AR(psi, phi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build A(R(ψ,ϕ)). Returns the formula A(R(ψ,ϕ)) where ψ and ϕ are the method parameters.

```APIDOC
## AR(psi, phi)

### Description
A shortcut to build A(R(ψ,ϕ)). Returns the formula A(R(ψ,ϕ)) where ψ and ϕ are the method parameters.

### Method
AR

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.
- **phi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula A(R(ψ,ϕ)).
```

--------------------------------

### Create and manipulate a DiGraph

Source: https://pymodelchecking.readthedocs.io/en/latest/using_models.html

Constructs a directed graph with vertices and edges, then shows how to access nodes and edges, and add a new edge.

```python
>>> from pyModelChecking import *
>>> G = DiGraph(V=['a',3],
...             E=[('a','a'), ('a','b')])
>>> print(G)

(V=['a', 3, 'b'], E=[('a', 'a'), ('a', 'b')])

>>> G.nodes()

['a', 3, 'b']

>>> G.edges()

[('a','a'), ('a','b')]

>>> G.add_edge('c','b')
>>> G.nodes()

['a', 'c', 3, 'b']

>>> G.edges()

[('a', 'a'), ('a', 'b'), ('c', 'b')]
```

--------------------------------

### EG() (in module pyModelChecking.CTL.language)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

CTL formula constructor for 'exists globally'.

```APIDOC
## EG() (in module pyModelChecking.CTL.language)

### Description
CTL formula constructor for 'exists globally'.
```

--------------------------------

### EU() (in module pyModelChecking.CTL.language)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

CTL formula constructor for 'exists until'.

```APIDOC
## EU() (in module pyModelChecking.CTL.language)

### Description
CTL formula constructor for 'exists until'.
```

--------------------------------

### AU(psi, phi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build A(U(ψ,ϕ)). Returns the formula A(U(ψ,ϕ)) where ψ and ϕ are the method parameters.

```APIDOC
## AU(psi, phi)

### Description
A shortcut to build A(U(ψ,ϕ)). Returns the formula A(U(ψ,ϕ)) where ψ and ϕ are the method parameters.

### Method
AU

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.
- **phi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula A(U(ψ,ϕ)).
```

--------------------------------

### AtomicProposition.__init__

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/PL/language.html

Initializes an atomic proposition with a given name. The name must be a string.

```APIDOC
## AtomicProposition.__init__

### Description
Initializes an atomic proposition with a given name. The name must be a string.

### Method
__init__

### Signature
__init__(self, name)

### Parameters
- **name** (str) - Required - The name of the atomic proposition.

### Returns
None

### Raises
- **TypeError** - If name is not a string.
```

--------------------------------

### Bool.__init__

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTLS/language.html

Initializes a Boolean atomic proposition with a given boolean value.

```APIDOC
## Bool.__init__

### Description
Initializes a Boolean atomic proposition with a given boolean value.

### Method
Constructor

### Parameters
- **value** (bool) - Required - The boolean atomic proposition.

### Example
```python
Bool(True)
```
```

--------------------------------

### AU

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/CTL/language.html

A shortcut to build the CTL formula A(U(psi, phi)).

```APIDOC
## AU

### Description
A shortcut to build the CTL formula A(U(psi, phi)).

### Method
`AU(psi, phi)`

### Parameters
- `psi` (CTL.StateFormula) - Required - A state formula.
- `phi` (CTL.StateFormula) - Required - A state formula.

### Returns
- (CTL.StateFormula) - The formula A(U(psi, phi)).

### Example
```python
formula = AU(p, q)
```
```

--------------------------------

### get_fair_states() (pyModelChecking.kripke.Kripke method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns the fair states of a Kripke structure.

```APIDOC
## get_fair_states() (pyModelChecking.kripke.Kripke method)

### Description
Returns the fair states of a Kripke structure.
```

--------------------------------

### Kripke.next(src)

Source: https://pymodelchecking.readthedocs.io/en/latest/_modules/pyModelChecking/kripke.html

Returns the set of successor states for a given source state, i.e., all states reachable via an edge from the source.

```APIDOC
## Kripke.next(src)

### Description
Returns the set of successor states for a given source state, i.e., all states reachable via an edge from the source.

### Parameters
- **src** - Required - The source state.

### Returns
- **set** - The set of nodes {s' | (src, s') in R}.

### Raises
- **RuntimeError** - If the source state is not a state of the Kripke structure.
```

--------------------------------

### get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.A method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns an equivalent non-fair formula for a CTLS A formula.

```APIDOC
## get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.A method)

### Description
Returns an equivalent non-fair formula for a CTLS A formula.
```

--------------------------------

### Simplify negation with LNot

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Demonstrates the LNot function that returns a logically equivalent formula with minimized outermost negations. Shows its behavior on nested negations.

```python
>>> f = Not(Not(Not(And('p',Not('q')))))
>>> f

not not not (p and not q)

>>> LNot(f)

(p and not q)

>>> LNot(Not(f))

not (p and not q)

>>> LNot(LNot(f))

not (p and not q)

```

--------------------------------

### get_equivalent_non_fair_formula() (pyModelChecking.CTL.language.A method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns an equivalent non-fair formula for a CTL A formula.

```APIDOC
## get_equivalent_non_fair_formula() (pyModelChecking.CTL.language.A method)

### Description
Returns an equivalent non-fair formula for a CTL A formula.
```

--------------------------------

### Parse CTL* Formula

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Shows how to use the CTLS Parser to parse CTL* formulas and combine them with operators.

```APIDOC
## Parse CTL* Formula

### Description
Use the CTLS Parser to parse CTL* formulas and combine them with operators.

### Usage
```python
from pyModelChecking.CTLS import *

p = Parser()
formula = p('G(not Heat)') | p('A(F(not Error))')
```

### Notes
- The CTLS Parser implements CTL* specific versions of operators ~, &, and |.
```

--------------------------------

### ER(psi, phi)

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A shortcut to build E(R(ψ,ϕ)). Returns the formula E(R(ψ,ϕ)) where ψ and ϕ are the method parameters.

```APIDOC
## ER(psi, phi)

### Description
A shortcut to build E(R(ψ,ϕ)). Returns the formula E(R(ψ,ϕ)) where ψ and ϕ are the method parameters.

### Method
ER

### Parameters
#### Arguments
- **psi** (CTL.StateFormula) - Required - A state formula.
- **phi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula E(R(ψ,ϕ)).
```

--------------------------------

### get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.E method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns an equivalent non-fair formula for a CTLS E formula.

```APIDOC
## get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.E method)

### Description
Returns an equivalent non-fair formula for a CTLS E formula.
```

--------------------------------

### get_equivalent_non_fair_formula() (pyModelChecking.CTL.language.E method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns an equivalent non-fair formula for a CTL E formula.

```APIDOC
## get_equivalent_non_fair_formula() (pyModelChecking.CTL.language.E method)

### Description
Returns an equivalent non-fair formula for a CTL E formula.
```

--------------------------------

### pyModelChecking.CTL.language.EX

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

Constructs the CTL formula E(X(ψ)).

```APIDOC
## pyModelChecking.CTL.language.EX

### Description
Constructs the CTL formula E(X(ψ)).

### Method
Constructor

### Parameters
- **psi** (CTL.StateFormula) - Required - A state formula.

### Returns
- **CTL.StateFormula** - The formula E(X(ψ)).
```

--------------------------------

### get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.Formula method)

Source: https://pymodelchecking.readthedocs.io/en/latest/genindex.html

Returns an equivalent non-fair formula for a CTLS formula.

```APIDOC
## get_equivalent_non_fair_formula() (pyModelChecking.CTLS.language.Formula method)

### Description
Returns an equivalent non-fair formula for a CTLS formula.
```

--------------------------------

### Define CTL* formula with A, G, Imply, And, Not, Or, F

Source: https://pymodelchecking.readthedocs.io/en/latest/using_logics.html

Constructs a CTL* formula using path quantifier A and temporal operators G and F, with logical connectives. The formula is displayed in a simplified syntax.

```python
>>> phi = A(G(
...         Imply(And(Not('Close'),
...                   'Start'),
...               A(Or(G(Not('Heat')),
...                    F(Not('Error')))))
...         ))
>>> phi

A(G(((not Close and Start) --> A((G(not Heat) or F(not Error))))))

```

--------------------------------

### pyModelChecking.CTL.language.X

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A class representing CTL X-formulas.

```APIDOC
## pyModelChecking.CTL.language.X

### Description
A class representing CTL X-formulas.

### Method
Constructor

### Parameters
- **phi** (tuple) - Required - The formula arguments.

### Returns
- **CTL.PathFormula** - An instance of the X-formula class.
```

--------------------------------

### pyModelChecking.CTL.language.PathFormula

Source: https://pymodelchecking.readthedocs.io/en/latest/logics_API.html

A class representing CTL* path formulas.

```APIDOC
## pyModelChecking.CTL.language.PathFormula

### Description
A class representing CTL* path formulas.

### Method
Constructor

### Parameters
- **phi** (tuple) - Required - The formula arguments.

### Returns
- **CTL.PathFormula** - An instance of the PathFormula class.
```
Tokens:
Raw