Documentation • Python/notebook interface

API of pypint module

When loaded, the pypint module will perform the follow tasks:

  • add Pint third-party binary path (bin subdirectory of pint-config share-path) to the PATH environment variable.

  • if in IPython, displays the version of Pint binaries, and executes ipython_install().

Pint types

ternary(b)

Returns ternary variable representation of b: either True, False, or Inconc. If b is None, returns Inconc.

class Conditions(*args)

Bases: dict

Used to represent conditions of transitions. They are modeled as standard dictionnary, associating automata to the required local states.

__str__()

Pint text representation of a condition.

class LocalTransition(a, i, j, conds)

Bases: object

A local transition within a single automaton.

An instance has 4 attributes:

  • a: name of the automaton

  • i: initial local state of a

  • j: final local state of a after the transition

  • conds: Conditions object

__repr__()

Pint text representation of a local transition

ctl_bifurcation(goal)

Returns the CTL specification for this transition being a bifurcation transition for goal.

modified_automata

Set of automata in which the local transition takes place ([a])

class SynchronizedLocalTransitions(aijs, conds)

Bases: object

Synchronized local transitions.

An instance has 2 attributes:

  • local_transitions: a list of (a,i,j) tuples representing the local transitions acting (always) synchronously

  • conds: Conditions object

__repr__()

Pint text representation of synchronized local transitions.

ctl_bifurcation(goal)

Returns the CTL specification for this transition being a bifurcation transition for goal.

modified_automata

Set of automata in which the local transitions take place.

local_transition_from_json(tup)

Converts a JSON representation of a local transition (as return by Pint executables) to either LocalTransition or SynchronizedLocalTransitions.

class Goal(*args, **kwargs)

Bases: object

Object which represents reachability goal used in most of Pint commands.

In its simplest form, a goal is the local state of an automaton. A goal can also be a sequence of sub-states.

It can be instanciated either with arguments or keywords (but not both). If instanciated with arguments, each argument specifies a sub-state, and the goal is the sequence of these sub-states. A sub-state can be specified either by a string (in pint format), or by a dict-like object. If instanciated with keywords, the goal is a single sub-state where the keys correspond to the automata and the values their local states.

Finally, alternative goals can be constructed using the operator | on the instanciated individual goals (see Goal.__or__()).

Examples:

>>> Goal(a=1)          # simple goal
>>> Goal((a,1))        # equivalent to above
>>> Goal("a=1")        # equivalent to above
>>> Goal(a=1,b=1)      # single sub-state goal
>>> Goal("a=1,b=1")    # equivalent to above
>>> Goal("a=1", "b=1") # sequence of simple goals
>>> Goal({"a": 1, "b": 1}, {"a": 0})    # sequence of sub-state goals
>>> Goal(a=1) | Goal(b=1)  # alternative goals
__or__(g2)

Construction of alternative goals: the returned goal consists of the disjunction of g1 and g2 (at least one of the two goals have to be reached).

Return type

Goal

__str__()

Return str(self).

automata

Returns the set of automata that are part of the goal specification

classmethod from_arg(arg, **kwargs)

Returns a Goal instance corresponding to arg

is_simple_goal

True iff the goal is only the local state of one automaton

is_state_formula()

True iff the goal corresponds to a state formula (no sequence of goals)

to_ctl()

Returns the CTL specification of the goal

to_pint()

Returns the argument to append to Pint commands for goal specification

pint_of_localstates(items)

Returns Pint text representation of a list of local states

Model input and analysis

LOAD_SUPPORTED_FORMATS = ['an', 'biocham', 'booleannet', 'boolfunctions', 'boolsim', 'cadbiom', 'ginml', 'sbgnpd', 'sbml', 'zginml']

Formats supported by load() method

load(filename=None, format=None, simplify=True, **opts)

Load a Pint model from given filename. The format is guessed from the filename extension, but can be enforced with the format parameter. Except when loading directly from a .an file (native format for Pint), the model will be converted to .an and a simplification step is performed. This latter stage can be deactivated with simplify=False

filename can be either a path to local file, or an URL. In the latter case, it will be downloaded locally first, and then processed as a local file.

Within IPython/Jupyter web notebook, the filename argument can be omited: in that case, a file upload form will be displayed.

Supported file extensions:

  • .an (automata network), native Pint file format;

  • .ginml, imported using GINsim (require ginsim Python module)

  • .zginml, like ginml, with in addition the support of named initial states;

  • .sbml (SBML-qual), imported using GINsim (require ginsim Python module);

  • .boolsim, .booleannet, .boolfunctions (or .bn): Boolean network formats, imported using GINsim (require ginsim Python module)`.

  • .bc: Biocham model - the importation implements its Boolean semantics (experimental feature)

Supported URL schemes:

  • CellCollective models can be imported by supplying the URL of the model main page. The SBML file location is determined automatically;

  • any other URL is treated as a link to a file with supported extension. It will be downloaded and then loaded as a local file.

Returns a Model instance. If the model results from an importation, IPython displays the link to the generated .an file.

Examples:

>>> m1 = pypint.load("mylocalfile.an")
>>> m2 = pypint.load("http://ginsim.org/sites/default/files/Frontiers-Th-Full-model-annotated.zginml")
>>> m3 = pypint.load("https://cellcollective.org/#4705/septation-initiation-network")

See also

LOAD_SUPPORTED_FORMATS for supported formats.

class Model

Bases: object

Abstract class for manipulating and analyzing an AN (Automata Network) model.

A Model is typically instanciated using the load() function, or using InMemoryModel for small in-memory AN specifications.

automata

The list of automata names

local_states

Dictionnary associating to each automaton its list of local states (str or int list).

local_transitions

The list of local transitions (LocalTransition or SynchronizedLocalTransitions) in the AN specification.

initial_state

The current initial state of the model (InitialState instance).

named_states

A dictionnary of named InitialState instances.

features

A list of features the AN model is using, if any, among:

  • “synced_transitions”: the AN uses synchronized local transitions.

automaton_graph(a)

Returns the directed graph of local transitions between the local states of automaton a. Edges are labeled with the index of the transitions in local_transitions.

Return type

NetworkX digraph (nx.DiGraph)

bifurcations(goal=None, method='ua', timeout=None, **kwgoal)

Identify local transitions after which, in some state, goal is no longer reachable.

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • method (str) –

    • "exact", "nusmv", or "its" for complete identification of bifurcation

      transitions (PSPACE); "exact" is an alias for "nusmv".

    • "ua+mole" for under-approximation relying on exact the reachable states set prior computation (NP+PSPACE)

    • "ua" for under-approximation of bifurcation transitions (NP)

  • timeout (int) – command timeout in seconds

Return type

LocalTransition list

count_reachable_states(tool='pint', timeout=None)

Counts the exact number of states reachable from initial_state. Uses an explicit state space approach.

Parameters
  • tool (str) –

    • "pint" explicit reachable state space computation (default);

    • "its" symbolic reable stae space computation

  • timeout (int) – command timeout in seconds

Return type

int

ctl_of_cutset(cutset, goal=None, **kwgoal)

Return the CTL specification for cutset being a cut-set for goal reachability.

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • cutset (list(dict[str,int or int list])) – cut-set

cutsets(goal=None, maxsize=5, exclude=[], exclude_initial_state=False, exclude_goal_automata=True, timeout=None, **kwgoal)

Computes sets of local states which are used in all the paths from the initial state to goal: if all the local states in a cut-set are disabled (all related local transitions are removed), then it is impossible to reach goal from the initial state.

Elements of the returned lists can be notably used as argument for methods Model.having() and disable().

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • maxsize (int) – maximal cardinality of a cut-set.

  • exclude (set(str)) – set/list of automata to exclude from the solutions

  • exclude_initial_state (bool) – if True, cut-sets can not be composed of initial local states.

  • exclude_goal_automata (bool) – exclude automata involved in the goal specification

  • timeout (int) – command timeout in seconds

Return type

list(dict[str,int or int list])

See also

method oneshot_mutations_for_cut()

dependency_graph()

Returns the dependency graph between automata: there is an edge from a to b if some local transitions of b depends on a.

Complexity: linear with the number of local transitions.

Return type

NetworkX digraph (nx.DiGraph)

disable(local_states=[], **kwstate)

Returns the AN where all local transitions involving specified local states have been removed.

Parameters
  • local_states (list(tuple(str,int)) or dict[str,int]) – local states to disable.

  • kwstate – complementary specification of local states.

Returns

a new FileModel instance for the modified AN.

export(format, output=None, reduce_for_goal=None, raw_args=None)

Export the AN model to the given format. If not provided the output filename is generated using new_output_file() and the extension corresponding to the export format.

  1. seealso:: EXPORT_SUPPORTED_FORMATS, and similar method save_as()

fixpoints(timeout=None)

Returns the complete list of fixed points of the model.

Parameters

timeout (int) – command timeout in seconds

Return type

dict list

full_lcg()

Shortcut for local_causality_graph() with kind=”full”

having(initial_state=None, **kwargs)

Returns a copy of the model with supplied modifications

Parameters
Return type

Model

Exemples:

>>> m.having(m.named_states["ProT1"]).reachability("Tf1=1")
>>> m.having(HR=1).reachability("Tf1=1")
local_causality_graph(kind='full', goal=None, **kwgoal)

Computes the Local Causality Graph (LCG) of type kind.

Parameters
  • kind (str) –

    • "full": LCG for all possible objectives from all possible initial states.

    • "verbose": LCG for simple over-approximation of goal rechability

    • "trimmed": LCG for simple over-approximation of goal reachability where impossible objectives have been removed.

    • "saturated": LCG for under-approximation of goal reachability

    • "worth": LCG used for goal-oriented reduction (see reduce())

  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1") when kind is not "full".

  • kwgoal – keywords for goal specification (instead of goal argument)

Return type

NetworkX multigraph (nx.MultiDiGraph)

lock(substate={}, **kwstate)

Returns the AN where the specified automata are lock to the given local state. The initial state is modified accordingly.

Parameters
  • substate (list(tuple(str,int)) or dict[str,int]) – local states to lock.

  • kwstate – complementary specification of local states.

Returns

a new FileModel instance for the modified AN.

oneshot_mutations_for_cut(goal=None, maxsize=5, exclude=[], exclude_goal_automata=True, timeout=None, **kwgoal)

Computes sets of local states for which the locking in the initial state ensures that goal is impossible to reach.

Elements of the returned lists can be notably used as argument for methods Model.having() and lock().

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • maxsize (int) – maximal cardinality of returned sets.

  • exclude (set(str)) – set/list of automata to exclude from the solutions

  • exclude_goal_automata (bool) – exclude automata involved in the goal specification

  • timeout (int) – command timeout in seconds

Return type

list(dict[str,int])

reachability(goal=None, fallback='its', tool='sa', sa_args=[], reduce_for_goal=True, timeout=None, **kwgoal)

Check if goal is reachable from the initial state. At first, Pint tries static analysis for the verification. If non-conclusive, it can fallback to exact model-checking.

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • fallback (str) – fallback to exact model-checking if static analysis is not conclusive. Supported model-checkers are: "its", "nusmv", and "mole".

  • tool (str) – tool for the model-checking: * "sa": static analysis with potential fallback method if not conclusive * "its", "nusmv", "mole": directly use the specified model-checker.

  • sa_args (list(str)) – additional arguments for static analysis

  • reduce_for_goal (bool) – before invoking a model-checker, perform the goal-oriented reduction of the automata network

  • timeout (int) – command timeout in seconds

Returns

  • True if goal is reachable from initial_state

  • False if goal is not reachable from initial_state

  • Inconc if the static analysis is not conclusive and fallback is None.

reachable_attractors(timeout=None)

Returns the complete list of attractors reachable from initial_state.

Uses an explicit state space exploration methods.

Parameters

timeout (int) – command timeout in seconds

Each attractor is described by a dict object with the following keys:

  • "type": either "fixpoint" or "cyclic".

  • "size": number of states in the attractor (1 if fixpoint, >1 if cyclic).

  • "sample": state (represented as dict) belonging to the attractor, i.e., either the fixpoint, or one of the state in the cycle attractor.

reachable_stategraph(timeout=None)

Returns the reachable state graph from initial_state.

Parameters

timeout (int) – command timeout in seconds

Return type

NetworkX digraph (nx.DiGraph)

reachable_states(timeout=None)

Returns the list of states reachable from initial_state.

Parameters

timeout (int) – command timeout in seconds

Return type

state list

reduce_for_goal(goal=None, squeeze=True, squeeze_preserve=None, **kwgoal)

Compute the goal-oriented reduction of the automata network. The reduction removes local transitions that are guaranteed to never contribute to any minimal path from the initial state to the goal (a path is minimal if there exists no paths using a strict subset of transitions leading to the goal).

The reduced models preserves existential reachability properties, as well as cut sets.

The complexity of the method is polynomial in the number of local transitions and automata, and exponential in the size of the largest automata minus 1.

Parameters
  • goal (str or list(str) or Goal) – goal specification (e.g., "a=1")

  • kwgoal – keywords for goal specification (instead of goal argument)

  • squeeze (bool) – if True (default), unused automata and local states are removed. Warning: this can lead to local state renaming.

  • list squeeze_preserve (str) – do not squeeze the given automata

Returns

a new FileModel instance for the reduced automata network.

Example:

>>> redm = m.reduce_for_goal("g=1")
register_state(name, state)

Register a named state in named_states attribute.

Parameters
  • name (str) – name of the state

  • state (dict or InitialState) – state to register

saturated_lcg(goal, **kwgoal)

Shortcut for local_causality_graph() with kind=”saturated”

save_as(filename)

Save the AN model with its initial state to local file filename. The format is guessed from the extension of filename.

See also

EXPORT_SUPPORTED_EXTENSIONS, and similar method export()

Examples:

>>> m.save_as("mymodel.an") # save to a local file in Pint native format
>>> m.save_as("mymodel.ll") # export in PEP format (Petri net)
simple_lcg(goal=None, **kwgoal)

Shortcut for local_causality_graph() with kind=”trimmed”

simplify()

Simplify the local transitions by computing their prime implicants.

Returns

a new FileModel instance for the reduced automata network.

summary()

Returns a dictionnary with various information on the AN model:

  • "nb_automata": number of automata (equivalent to len(m.automata))

  • "nb_local_states": total number of local states

  • "max_local_states": largest number of local states within one automaton.

  • "nb_transitions": number of local transitions

  • "nb_states": total number of states

Return type

dict

to_its(reduce_for_goal=None)

TODO

Parameters

reduce_for_goal (str or list(str) or Goal) – perform goal-oriented model reduction before exportation.

to_nusmv(skip_init=True, existential_ctx=True, reduce_for_goal=None)

TODO

Parameters
  • skip_init (bool) – do not generate an INIT statement.

  • existential_ctx (bool) – if True (default), whenever the initial state is partial, the properties have to hold from at least one complete initial state; if False, the properties have to hold from all the possible complete initial states.

  • reduce_for_goal (str or list(str) or Goal) – perform goal-oriented model reduction before exportation.

worth_lcg(goal, **kwgoal)

Shortcut for local_causality_graph() with kind=”worth”

class FileModel(filename)

Bases: pypint.model.Model

Concrete class of Model for AN model stored in a local file.

source()

Returns the text source in Pint native format

class InMemoryModel(data)

Bases: pypint.model.Model

Concrete class of Model for an AN model stored in memory.

source()

Returns the text source in Pint native format

class InitialState(state)

Bases: dict

A state is represented with a dict-like python object, which associates each automaton to a local state, or to a set of initial local states.

The automata, their value domain, as well as their initial default value, are tied to a Model object.

A new InitialState should be instanciated only from an existing InitialState instance, typically Model.initial_state, either using the copy constructor, or using InitialState.copy(), or using InitialState.having() method (recommended).

changes()
Returns

A dict object of the changes to the default initial state.

copy()
Returns

a copy of the object.

having(*args, **kwargs)
Returns

a copy of the object modified with update() method.

is_custom()
Returns

True iff the state is different from the default initial state of the AN.

nonzeros()
Returns

A dict object associating automata to their initial local states when it is different from 0.

reset()

Restore to default initial state.

to_pint(full=False)
Returns

Pint text representation of the state

Parameters

full – if True, also output initial states being 0.

update(*args, **F)

Sets the initial local states of specified automata. Arguments can be either dict-like objects, lists of pairs or keywords.

Examples:

>>> s.update(a=1, b=0)  # updates automaton 'a' and 'b'
>>> s.update({"a": 1, "b": 0})  # equivalent to above
EXPORT_SUPPORTED_FORMATS = ['asp', 'dump', 'nusmv', 'pep', 'pnml', 'romeo']

Formats supported by Model.export() method.

EXPORT_SUPPORTED_EXTENSIONS = ['an', 'asp', 'll', 'lp', 'pnml', 'smv', 'xml']

File extensions supported by Model.save_as() method:

  • .an: Pint native format

  • .ll: PEP format (Petri net)

  • .pnml: PNML format (Petri net)

  • .smv: NuSMV format

  • .xml: Romeo format (Petri net)

exception PintProcessError(returncode, cmd, output=None, stderr=None)

Bases: subprocess.CalledProcessError

Exception raised when a Pint command fails.

Helper functions

file_ext(filename)

Returns the extension of filename in lower case; or None if there is no extension

Setup functions

CFG = {'console': False, 'dbg': False}

Python module configuation:

data_file(name)

Returns path to file name distributed with pypint.

output_dir()

Creates the output directory and returns its path

new_output_file(ext=None, **tempargs)

Creates a new file in output_dir() using tempfile.mkstemp and returns its path. The parameter ext specifies the extension of the file; tempargs are forwarded to tempfile.mkstemp with prefix=colomoto by default.

remove_output_files()

Removes files created by colomoto if autoclean=True, and in particular if preserve_output_files() has not been called.

User interface functions

dbg(msg)

If debug is enabled, print msg (prefixed with ‘#’)

enable_dbg()

Enable debug output (executed command lines, etc.)

disable_dbg()

Disable debug output (executed command lines, etc.)

info(msg)

Print msg (note: in IPython, msg is interpreted in Markdown format)