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 thePATH
environment variable.if in IPython, displays the version of Pint binaries, and executes
ipython_install()
.
Content
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
orSynchronizedLocalTransitions
.
-
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 (seeGoal.__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
-
__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=Falsefilename 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 usingInMemoryModel
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
orSynchronizedLocalTransitions
) 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 bifurcationtransitions (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()
anddisable()
.- 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.seealso::
EXPORT_SUPPORTED_FORMATS
, and similar methodsave_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
initial_state (InitialState or str) – new initial state
kwargs – if non-empty, defines a new initial state from
Model.initial_state
by callingInitialState.having()
.
- Return type
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 (seereduce()
)
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()
andlock()
.- 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 frominitial_state
False
if goal is not reachable frominitial_state
Inconc
if the static analysis is not conclusive and fallback isNone
.
-
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 methodexport()
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 usingInitialState.copy()
, or usingInitialState.having()
method (recommended).-
changes
()¶ - Returns
A dict object of the changes to the default initial state.
-
copy
()¶ - Returns
a copy of the object.
-
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:
dbg: enable debug output (see also
enable_dbg()
,disable_dbg()
,dbg()
).console: assume console output
-
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 totempfile.mkstemp
withprefix=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.