When ecco is loaded as %run -m ecco myfile.rr, it loads and parse myfile.rr and provides an instance of class Model called model, which is the entry point for analysis the model.
class Model
Options:
traps: bool = False: whether traps should be computed automatically or not
method __call__()
def __call__(self, *split, /, _init=None, **aliased): ...
Build a cg.ComponentGraph from the model.
Aguments
_init (None): initial state given as adictmapping variable names to sets of initial valuessplit, ...: arguments suitable toComponentGraph.split()in order to perform an initial split (if none is given, the graph will have just one component with all the reachable states)alias=prop, ...: other arguments forComponentGraph.split()
Return
A cg.ComponentGraph instance, possibly split as specified.
method charact()
def charact(self, constraints=True, variables=None, plot=True): ...
Show variables characterisation.
This is a table that counts for each variable how many time it is read and how many times it is assigned.
Arguments
constraints (bool=True): shall constraints be taken into accountvariables (None): list of variables to include, or a function that take a variable name and return aboolplot (bool=True): ifTrueadd bars to the table to be displayed in Jupyter, otherwise, just return the data
Return
- a styled
pd.io.formats.style.Stylerifplot=True - a raw
pd.DataFrameifplot=False
method ecograph()
def ecograph(self, constraints=True, **opt): ...
Show the ecosystemic graph.
The nodes are the variables and an edge from one variable to another
means that the former has an influence onto the latter. there are two
possible reasons for a variable x to have an influence onto y:
xappears in the left-hand side of an actions andyis assigned in the right-hand sign, eg:x+ >> y+yis assigned with an expression involvingx, butxis not necessarily a condition of the action, eg:... >> y=x+1
Arguments
constraints (bool=True): whether to take the constraints into accountkey=val, ...: any option suitable forcygraphs.Graph
Return
A cygraph.Graph instance that can be directly displayed in Jupyter.
method ecohyper()
def ecohyper(self, constraints=True, **opt): ...
Show the ecosystemic hypergraph.
This is an evolution of the ecosystemic graph that is more detailed and precise. For each action, its has a square node that is linked to all the variables (round nodes) it involves. This links can have several tips:
- a white dot at the action end means that the action expects the variable to be off
- a black dot at the action end means that the action expects the variable to be on
- no tip at the action end means that the action does not read the variable
- a white dot at the variable end means that the action sets the variable to off
- a black dot at the variable end means that the action sets the variable to on
- no tip at the action end means that the action does not assign the variable
Arguments
constraints (bool=True): whether to take the constraints into accountkey=val, ...: any option suitable forcygraphs.Graph
Return
A cygraph.Graph instance that can be directly displayed in Jupyter.
method expand()
def expand(self, out=<_io.TextIOWrapper name='<stdout>' mode='w' encoding='utf-8'>): ...
property rr
Show RR source code.
The code shown is reconstructed from parsed source, so it may have some differences with it (and is usually clearer).
class ComponentGraph
A ComponentGraph is a decomposition of a state-space.
Its nodes are pairwise-disjoint symbolic sets of states, called components, and its edges are the explicit transitions allowing to reach one component from another. Usually, the union of components is the set of the reachable states, but user may drop components and so get just a subset of the reachable states.
Note that in every method accepting arbitrary arguments **arg, there may
be specific keyword arguments that are then starting with _.
Two enumerated types are used together with ComponentGraph:
setrelwhose values areHASNO,HAS,CONTAINS,ISIN, andEQUALStopowhose values areINIT,ENTRY,EXIT,HULL,DEAD, andSCC
method has_traps()
def has_traps(self): ...
Tells whether (some) traps have been computed or not.
method traps()
def traps(self, *args): ...
Compute traps.
Method traps(...) compute whether the edges entering the given nodes
(all if none given) are trapped, and thus whether the nodes themselves are.
An edge entering a node is trapped if it does not allow to reach every exit
of this node. In such a case, the component graphs shows paths that are not
always feasible. Hence the trap. When traps are computed, a column trap is
added to the .edges table showing whether each edge is trapped or not. A
node is trapped if it has trapped entering edges. When traps are computed,
a column traps is added to the .nodes table showing the components from
which a trapped arc is incoming.
Arguments
int, ...: a series of components number, if empty, all the components in the graph are considered
Return
A dict associating each argument component to its incoming nodes that cause
a trap. For instance, if g.traps(1, 2) returns {1: {3, 4}, 2: {5}},
it means that (3, 1), (4, 1), and (5, 2) are trapped edges (and others
entering 1 or 2 are not).
method untrap()
def untrap(self, *args, /, _recurse=False): ...
Remove traps from nodes.
A trap in a node n is defined by an input node i and the set t of
states that i allows to reach through n. If t does not reach all the
successor nodes of n, then this is a trap and this method splits n into
n & t and n - t. Doing so, new traps may be created on the new nodes,
in which case untrap should be applied recursively until no traps remain.
Note that traps will be removed only from nodes on which they have been
detected already. So, traps() and untrap() should be called consistently.
(More precisely, in traps were not computed for a given node, then untrap
will ignore it.)
Arguments
int, ...: a series of components number, if empty, all the components in the graph are considered_recurse (bool=True): shalluntrapbe applied recursively
Return
A new ComponentGraph (or the original one if no split occurred).
method walk()
def walk(self, *nodes, **filters): ...
General API
method __len__()
def __len__(self): ...
Return the number of Components in the ComponentGraph.
method __eq__()
def __eq__(self, other): ...
Check for equality of two ComponentGraphs.
They are equal if the contain exactly the same set of components.
method __getitem__()
def __getitem__(self, key): ...
Return a node or an edge.
Arguments
key (int): return aComponentfrom its number- or
key (int,int): return an edge from the number of its source/destination nodes, that is its attributes as found in the.edgestable
Return
Component or dict.
method __iter__()
def __iter__(self): ...
Yield every Component in the ComponentGraph.
Attributes
property nodes
The nodes table holds all about the nodes of a ComponentGraph.
This is stored as a pandas.DataFrame
whose columns are:
index: component numbersize: number of states in the componentconsts: set of constants in the component- one column for each
relinsetrel: for each relation, set of properties checked for the component that have this relation with its states, eg, if proppis in columnISINthis means that the set of states of the component is included in the sate of states that satisfypin the whole LTS
property n
A proxy to .nodes table.
- when printed,
.nshows a summary of the content of.nodes - so do printing
.n[col]or.n[[col, ...]] - deleting
.n[col]or.n[col, ...]deletes columns in.nodes - setting
.n[col] = fun, wherefunis a function that takes a row as yield by.nodes.iterrows()and return a value, its creates and populates a new columncol
property edges
The edges table holds all about the edges of a ComponentGraph.
This is stored as a pandas.DataFrame
whose columns are:
src: source component numberdst: destination component numberactions: rules or constraints on this edgetags: the corresponding action labels
property e
A proxy to .edges table.
Works similarly as .n.
property g
The actual graph in the ComponentGraph.
This is stored as an igraph.Graph instance
whoses nodes are labelled with the component numbers and whose edges
are labelled with the source and destination component numbers as well
as with the transitions.
Properties management
method check()
def check(self, *args, /, _warn=True, **aliased): ...
Check properties on components.
Properties are expressed in one of the supported syntaxes (CTL, topological, or functional). Each property is evaluated globally on the LTS and then compared with the states of the considered components. Their relation is the recorded in the components and the nodes table. Properties may be aliased, that is, an alias is recorded instead of the property itself, this allow producing a simpler nodes table with short property names instead of complex expressions.
Arguments
str, ...: at least of property to be checkedint, ...: the components on which to check the properties, if none is given, all the components are used_warn (bool=True): shall we print a warning if a property is found to match no statesalias=prop, ...: aliased properties
Return
A dict that maps each checked component to a dict that
itself maps each checked property to the corresponding setrel.
method tag()
def tag(self, *args): ...
Tag components with arbitrary properties.
Arbitrary properties mean that they are just str that are associated
to the states of the components. Thus they are tags rather that real
properties expressed in a particular syntax. Note that if several
components are passed, the states corresponding to the tag will be the
union of these components’ states.
Arguments
str, ...: at leat one tag to addint, ...: the components that should be tagged, if none is given, all the components are used
method forget()
def forget(self, *args): ...
Forget about properties in components.
Every specified component (or all if non are specified) will forget about every specified property.
Arguments
str, ...: a series of at least one property to forgetint, ...: a series of components that must forget about properties if none is given, all the components are used
method forget_all()
def forget_all(self, *args): ...
Forget about all properties forsome components.
Arguments
int, ...: the components that should forget about all properties, if none is given, all the components are used
method update()
def update(self): ...
Update the nodes table if new properties have been checked.
This method is normally called automatically, but if some Component
are updated directly, then update should be called.
Queries
method __call__()
def __call__(self, prop, rel=<setrel.HAS: 1>, strict=False): ...
Return the component numbers that match prop with relation rel.
If the property has not been checked already, check is called for it.
Matching can be strict, in which case exactly rel must be found. But
if matching is not strict, other relations can be considered, for
instance, non-strict HAS can match CONTAINS (if a component
contains a property, then is has its states), ISIN, and EQUALS.
The returned set can be complemented with ~, which allows to get
the components that do not match a property. Moreover, several such
queries can be combined using the usual sets operations.
Arguments
prop (str|topo): property to searchrel (setrel): expected relationstrict (bool=False): whether matching should be strict or not
Return
A set of matching component numbers.
method CONTAINS()
def CONTAINS(self, prop): ...
Shorthand for __call__(prop, setrel.CONTAINS, True).
method contains()
def contains(self, prop): ...
Shorthand for __call__(prop, setrel.CONTAINS, False).
method EQUALS()
def EQUALS(self, prop): ...
Shorthand for __call__(prop, setrel.EQUALS, True).
method equals()
def equals(self, prop): ...
Shorthand for __call__(prop, setrel.EQUALS, False).
method HAS()
def HAS(self, prop): ...
Shorthand for __call__(prop, setrel.HAS, True).
method has()
def has(self, prop): ...
Shorthand for __call__(prop, setrel.HAS, False).
method HASNO()
def HASNO(self, prop): ...
Shorthand for __call__(prop, setrel.HASNO, True).
method hasno()
def hasno(self, prop): ...
Shorthand for __call__(prop, setrel.HASNO, False).
method ISIN()
def ISIN(self, prop): ...
Shorthand for __call__(prop, setrel.ISIN, True).
method isin()
def isin(self, prop): ...
Shorthand for __call__(prop, setrel.ISIN, False).
method select()
def select(self, *args, /, _all=True, _rel=<setrel.ISIN: 3>, _strict=False, **aliased): ...
Return the component numbers that match all/any properties.
Given a series of properties props and series of components comps,
this method returns the subset of components among comps that match
all (if _all=True) or any (if _all=False) of the properties in
props. Additional properties may be given using aliased. Matching
is performed as in __call__ using _rel and _strict.
Arguments
str|topo, ...: at least one property to be matched against the states of componentsint, ...: the components on which to check the properties, if none is given, all the components are used_all (bool=True): whether components should match all or any of the properties_rel (setrel=ISIN): the relation used in matching_strict (bool=False): whether to perform strict matching or notalias=prop, ...: aliased properties to be matched with others
Return
The set of matching components.
method count()
def count(self, *args, /, transpose=False): ...
Count how many states have each variable in each value.
Argument
int, ...: the components to count in, or all if non is giventranspose (bool=True): transpose the matrix before to return it
Return
A pandas.DataFrame instance whose
columns are the component numbers and whose index is the list of
pairs var, val.
method form()
def form(self, *args, /, variables=None, normalise=None, separate=False): ...
Describe components by Boolean formulas.
Arguments
int, ...: a series of components number, if empty, all the components in the graph are consideredvariables=...: a collection of variables names to restrict tonormalise=...: how the formula should be normalised, which must be either:"cnf": conjunctive normal form"dnf": disjunctive normal formNone: chose the smallest form
separate=...: ifFalse(default) returns a single formula, otherwise, returns one formula for each considered component
Return
A SymPy Boolean formula
or a dict mapping component numbers to such formulas.
Splits
method split()
def split(self, *args, /, _warn=True, _limit=256, _progress=False, **aliased): ...
Split components with respect to properties.
For each given property, the given components are split into the part
that validate the property and the part that doesn’t. Properties may
be formulas given as str in one of the available syntaxes, or topo
values. The properties used for splitting are recorded in the
components and the nodes tables, either as such or using an alias
if aliased is used.
Arguments
int, ...: components to be split, or all if non is givenstr|topo, ...: properties to be used for splitting_warn (bool=True): whether to issue a warning if a property is found to match no states_limit (int=256): ask a confirmation if splitting yields more that the given number of components, giving0disables confirmation_progress (bool=False): show a progress bar as splits are going onalias=prop, ...: specify aliased properties that are stored asaliasinstead ofpropin the components and the nodes table
Return
A new ComponentGraph (or the original one if no split occurred).
method explicit()
def explicit(self, *args, /, _limit=256): ...
Split components into their individual states.
Every provided component is split into its individual states.
Arguments
int, ...: components to be split, or all if non is given_limit (int=256): as forsplit()
Return
A new ComponentGraph (or the original one if no split occurred).
method classify()
def classify(self, *args, /, _split=True, _limit=256, _col=None, _src=None, _dst=None, **aliased): ...
Classify components against a set of aliased properties.
Every given component is checked or split against every given propery. A column is the added to the resulting nodes table to summarize in which class every resulting component is.
Arguments
int, ...: components to be classified, or all if none is given_split (bool=True): wether the classified components should be split wrt the properties or we shoud used the existing components as such_col (str=None): if notNoneadd a column_colin the resulting nodes table to summarize in which class every component is_src (str=None): add a column to the edges table with the classification of the source nodes_dst (str=None): add a column to the edges table with the classification of the destination nodesclassname=prop, ...: classes to be used and the corresponding properties
Return
A new ComponentGraph (or the original one with properties
updated if _split=False).
Other operations
method merge()
def merge(self, *args): ...
Merge components into a single one.
Arguments
int, int, ...: at least two components to be merged
Return
A new ComponentGraph.
method drop()
def drop(self, *args, /, _warn=True): ...
Drop some components.
Arguments
int, ...: at least one component to be dropped_warn (bool=True): issue a warning if all the components are to be dropped, which is not possible
Return
A new ComponentGraph (or None if all the components are to
be dropped).
method draw()
def draw(self, **opt): ...
Draw the component graph as an interactive cygraphs.Graph.
It accepts any option opt accepted by cygraphs.Graph and returns
an interactive cygraphs.Graph instance that can be directly displayed
in a Jupyter notebook when it is the result of the cell (otherwise,
use Jupyter’s function display).
method make_states()
def make_states(self, spec): ...
Parse a string as a partial valuation.
spec is expacted to be a comma-separated list of valuations, each
valuation being one of:
VAR=VAL, whereVARis a variable name andVALa value for itVAR+that is a shorthand forVAR=1VAR-that is a shorthand forVAR=0VAR*that is a shorthand forVAR=vfor allvin the domain ofVAR
The specified valuations are accumulated. Variables that have not been valuated are assumed to range on their domains.
Arguments
str spec: specification to be parsed
Return
A sdd containing the specifies states.
class cygraph.Graph
An interactive graph that can be displayed in Jupyter
method __init__()
def __init__(self, nodes, edges, **args): ...
Build a new Graph instance
Arguments
nodes: apandas.DataFramewith the nodes, it must have a columnnodewith the nodes identitesedges: apandas.DataFramewith the edges, it must have two columnssrcanddstwith the nodes sources and destination as provided innodes["node"]**args: varied options listed below
Most nodes and edges options may be given as a single value that
is applied to every nodes/edges, or as the name of a column in
nodes/edges tables containing the values to apply to each node/edge,
or as an array of values whose length is the number of
nodes/edges. When a column or an array is provided, it must
contain valid values for the expected property, except for the
color that can be computed in every case.
Graph options
layout (str|tuple[str,dict]): a layout algorithm, or a pair(algo, options)where options are the parameters for the chosen algorithmlayout_extra (dict): additional layout algorithms to be added to the UI, mapping names to functions or static positions
Layout algorithms are mainly provided by
Cytoscape.js or by
GraphViz (all those named gv-...).
Available layout algorithms are:
random: distribute nodes randomlygrid: distribute nodes on a rectangular gridcircleandgv-circo: distribute the nodes on a circleconcentricandgv-twopi: distribute the nodes on concentric circlesbreadthfirst: distribute the nodes hierarchically as a breadth-first spanning treecose,gv-neato,gv-fdp: distribute the nodes using a spring simulationdagreandgv-dot: distribute the nodes hierarchically
Colors
Colors are obtained from a pair of options ..._color and
..._palette as follows:
- a named color (
"red", etc.) is applied to evey nodes/edges - a HTML colors (
"#C0FFEE", etc.) also - a column/array of values is used to compute a color for each unique value according to the palette (see below)
A palette is provided as either:
- a name (
str) that maps to a series of colors, seePalette.palettes - an optional mode (one of
"lin"(default),"log", or"abs") that specifies how colors in the palette are interpolated- when
mode="lin"the set of unique values is linearly distributed onto the list of colors in the palette, and unique colors are computed by interpolation. - when
mode="log"the same principle is applied but the values are distributed on a logarithmic scale (values are close one to each other at the beginning and get farther as we move to the right) - when
mode="abs"the values must be numbers and are directly used as the position within the palette (after being scaled to the appropriate range)
- when
- an optional
bool(default:True) that specifies if values are sorted before to generate colors for them
Consider for example a palette of 4 colors with 5 unique values, they can be distributed linearly as:
palette: "#AFA" "#FAA" "#FF8" "#AAF"
values: a b c d e
The color for a will be "#AFA", the color for e will be
"#AAF", the color for c will be 50% "#FAA" and 50% "#FF8", the
color for b will be mostly "#FFA" with a touch of "#AFA", etc.
Nodes options
nodes_shape: shape as listed inTableShapeDesc.valuesnodes_width: width asintorfloatnodes_height: height asintorfloatnodes_size: both width and eight, asintorfloatnode_fill_color: background colornodes_fill_palette: palette for background colornodes_fill_opacity: background opacity (floatbetween0.0and1.0)nodes_image: images to use as nodes background, which may be a list of- paths to files relative to notebook, or
- URLs to images publicly available
nodes_draw_color: color for the border of nodesnodes_draw_palette: palette fornodes_draw_colornodes_draw_style: line style for the border of nodes, as listed inTableStyleDesc.valuesnodes_draw_width: line width for the border of nodesnodes_show: how to display nodes, specified as:"all": display all nodesmode, values: wherevaluesis a list of Boolean (one for each node) or a column innodestable, andmodeis one of:"dim"dim nodes for whichvaluesisTrue"hide"hide nodes for whichvaluesisTrue"drop"drop nodes for whichvaluesisTrue
mode, values, invert: as above withinvertbeing aboolto specify whethervaluesshould be negated or not"dim", values, invert, dimas above with0.0 <= dim <= 1.0to set dim level
A hidden node is still considered to compute layouts while a dropped node is (mostly) ignored. GraphViz layouts make no difference between both modes.
Node labels options
nodes_label: text drawn onto nodesnodes_label_wrap: how labels text is wrapped, as listed inTableWrapDesc.valuesnodes_label_size: size of labelsnodes_label_halign: horizontal placement of labels wrt nodes, as listed inTableHalignDesc.valuesnodes_label_valign: vertical placement of labels wrt nodes, as listed inTableValignDesc.valuesnode_label_align: both horizontal and vertical placement of labels wrt nodes, given as a one- ot two-charsstrcombining:"n"orth,"s"outh,"e"ast,"w"est,"c"enter, or"m"iddle (the last two are synonymous). If only one align is given, the other default to"m", for instance,"n"is equivalent to"nm"(or"nc"). If the first letter is"c"or"m", it will be used for horizontal alignment, so"cn"will fail because it specifies twice horizontal alignement. To avoid this, start with a character in"nsew"that is tight to one direction.nodes_label_angle: the rotation of labels, in degreesnodes_label_outline_width: width of the outline around node labelsnodes_label_outline_color: color of the outline around node labelsnodes_label_outline_palette: palette fornodes_label_outline_colornodes_label_outline_opacity: opacity of label outline
Edges options
edges_curve:- when
"bezier", two opposite edges will be bent automatically to avoid their overlapping, which is desired when they have labels - when
straight, two opposite edges will overlap, which may be desired when they have no labels
- when
edges_draw_color,edges_draw_palette,edges_draw_style, andedges_draw_width: likenodes_draw_...but for edges (which means that information is taken from tableedgesif column names are used)edges_label,edges_label_angle,edges_label_outline_width,edges_label_outline_color,edges_label_outline_palette,edges_label_outline_opacity: likenodes_label...but for edges. Note thatedges_label_angle="auto"allows to automatically rotate the label following the slope of each edge.
Edges tips
edges_tip_scale: scaling factor that applies to all edge tips, this is a single value (default0.6) and cannot be a column/array of valuesedges_target_tip: shape of edge tip at target node, as listed inTableTipDesc.values. Values may be prefixed with"filled-"or"hollow-"to fill or not the tip drawing.TableTipDesc.aliasprovides short names for some edge tips.edges_target_colorandedges_target_palette: color and palette of edge tips at target nodeedges_source_tip,edges_source_color,edges_source_palette: likeedges_source_...but for the tips as edges source
Coumpound options
Additional properties gather other properties, so assigning them will actually assign several other properties, and reading them will return a tuple of other properties:
nodes_color:nodes_draw_colorandnodes_fill_colornodes_palette:nodes_draw_paletteandnodes_fill_paletteedges_tip_color:edges_target_colorandedges_source_coloredges_tip_palette:edges_target_paletteandedges_source_paletteedges_color:edges_draw_colorandedges_tip_coloredges_palette:edges_draw_paletteandedges_tip_palette
User interface
User interface (UI) option ui may be given as a list of UI elements
organised as nested lists and dicts:
- top-level
listis a vbox, a vbox arranges its content into aipywidget.VBox - a
listin a vbox arranges its content into anipywidget.HBox - a
dictin a vbox arranges its content as anipywidget.Accordionwhose sections are the keys of the dict, each containing a vbox. - no other nesting is allowed
- atomic elements are:
- the name of an option listed above (except the coumpound ones) to build a widget allowing to tune this option
"graph": the interactive graph itself"reset_view": a button to recompute the layout and reset the graph display, which is useful when one has zoomed too much and the graph is not visible anymore"select_all","select_none", and"invert_selection": buttons to (un)select nodes"inspect_nodes"and"inspect_edges": view ofnodesandedgestables limited to the selected nodes and the edges connected to them. Optionsinspect_nodesandinspect_edgesmay be provided (as lists of columns) to restrict the columns displayed here
All the options presented above, except those related to the building of
the UI, are also attributes of a Graph instance. Which means they can be
read or assigned to change a graph appearance. In this case, it is
mandatory to call method update to actually update the display after
changing an option. Graph instance also supports item assignement
to update one option for just one node or edge, see __setitem__
documentation.
method __setitem__()
def __setitem__(self, key, val): ...
Update an option for one specific node or edge
For instance, to change nodes, we use "option":node indexing, and
for edges, we use "option":source:target indexing:
g = Graph(nodes, edges, nodes_fill_color="red", edges_color="red")
g["color":1] = "#C0FFEE" # node 1 is turned blue
g["color":1:2] = "#DEFEC7" # edge from 1 to 2 is turned green
g.update() # update display
"options" above is not prefixed by either "nodes_" or "edges_"
as this is deduced from the indexing used. So in the second line,
"color" is expanded to nodes_color option, and in the third line,
"color" is expanded to edges_color option. (Note that both are
compound options that gather several other ones.)