API reference

class Model

Store a model.

Attributes

• path: file path from which the model was loaded
• spec: the model itself
• base: base directory in which auxiliary files are stored

method __call__()

def __call__(self, *split, /, _init=None, **aliased): ...

Build a cg.ComponentGraph from the model.

Aguments

• _init (None): initial state given as a dict mapping variable names to sets of initial values
• split, ...: arguments suitable to ComponentGraph.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 for ComponentGraph.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 account
• variables (None): list of variables to include, or a function that take a variable name and return a bool
• plot (bool=True): if True add bars to the table to be displayed in Jupyter, otherwise, just return the data

Return

• a styled pd.io.formats.style.Styler if plot=True
• a raw pd.DataFrame if plot=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:

• x appears in the left-hand side of an actions and y is assigned in the right-hand sign, eg: x+ >> y+
• y is assigned with an expression involving x, but x is not necessarily a condition of the action, eg: ... >> y=x+1

Arguments

• constraints (bool=True): whether to take the constraints into account
• key=val, ...: any option suitable for cygraphs.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 account
• key=val, ...: any option suitable for cygraphs.Graph

Return

A cygraph.Graph instance that can be directly displayed in Jupyter.

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:

• setrel whose values are HASNO, HAS, CONTAINS, ISIN, and EQUALS
• topo whose values are INIT, ENTRY, EXIT, HULL, DEAD, and SCC

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 a Component from 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 .edges table

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 number
• size: number of states in the component
• consts: set of constants in the component
• one column for each rel in setrel: for each relation, set of properties checked for the component that have this relation with its states, eg, if prop p is in column ISIN this means that the set of states of the component is included in the sate of states that satisfy p in the whole LTS

property n

A proxy to .nodes table.

• when printed, .n shows 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, where fun is a function that takes a row as yield by .nodes.iterrows() and return a value, its creates and populates a new column col

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 number
• dst: destination component number
• actions: rules or constraints on this edge
• tags: 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 checked
• int, ...: 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 states
• alias=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 add
• int, ...: 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 forget
• int, ...: 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 search
• rel (setrel): expected relation
• strict (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 components
• int, ...: 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 not
• alias=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 given
• transpose (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 pca()

def pca(self, *args, /, transpose=False, n_components=2, n_iter=3, copy=True, check_input=True, engine='sklearn', random_state=42, rescale_with_mean=True, rescale_with_std=True): ...

Principal component analysis of the matrix returned by count().

Arguments

• int, ...: the components to count in, or all if non is given
• transpose (bool=True): passed to count()

For documentation about the other arguments, see Prince doc

Return

A pandas.DataFrame as computed by Prince.

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 considered
• variables=...: a collection of variables names to restrict to
• normalise=...: how the formula should be normalised, which must be either:
  • "cnf": conjunctive normal form
  • "dnf": disjunctive normal form
  • None: chose the smallest form
• separate=...: if False (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, **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 given
• str|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, giving 0 disables confirmation
• alias=prop, ...: specify aliased properties that are stored as alias instead of prop in 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 for split()

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 not None add a column _col in 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 nodes
• classname=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, where VAR is a variable name and VAL a value for it
• VAR+ that is a shorthand for VAR=1
• VAR- that is a shorthand for VAR=0
• VAR* that is a shorthand for VAR=v for all v in the domain of VAR

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: a pandas.DataFrame with the nodes, it must have a column node with the nodes identites
• edges: a pandas.DataFrame with the edges, it must have two columns src and dst with the nodes sources and destination as provided in nodes["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 algorithm
• layout_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 randomly
• grid: distribute nodes on a rectangular grid
• circle and gv-circo: distribute the nodes on a circle
• concentric and gv-twopi: distribute the nodes on concentric circles
• breadthfirst: distribute the nodes hierarchically as a breadth-first spanning tree
• cose, gv-neato, gv-fdp: distribute the nodes using a spring simulation
• dagre and gv-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, see Palette.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)
• 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 in TableShapeDesc.values
• nodes_width: width as int or float
• nodes_height: height as int or float
• nodes_size: both width and eight, as int or float
• node_fill_color: background color
• nodes_fill_palette: palette for background color
• nodes_fill_opacity: background opacity (float between 0.0 and 1.0)
• nodes_draw_color: color for the border of nodes
• nodes_draw_palette: palette for nodes_draw_color
• nodes_draw_style: line style for the border of nodes, as listed in TableStyleDesc.values
• nodes_draw_width: line width for the border of nodes
• nodes_show: how to display nodes, specified as:
  • "all": display all nodes
  • mode, values: where values is a list of Boolean (one for each node) or a column in nodes table, and mode is one of:
    • "dim" dim nodes for which values is True
    • "hide" hide nodes for which values is True
    • "drop" drop nodes for which values is True
  • mode, values, invert: as above with invert being a bool to specify whether values should be negated or not
  • "dim", values, invert, dim as above with 0.0 <= dim <= 1.0 to set dim level

A hidden node is still considered to compute layouts while a dropped node is (mostly) ignored. GraphViz or PCA layouts make no difference between both modes.

Node labels options

• nodes_label: text drawn onto nodes
• nodes_label_wrap: how labels text is wrapped, as listed in TableWrapDesc.values
• nodes_label_size: size of labels
• nodes_label_halign: horizontal placement of labels wrt nodes, as listed in TableHalignDesc.values
• nodes_label_valign: vertical placement of labels wrt nodes, as listed in TableValignDesc.values
• node_label_align: both horizontal and vertical placement of labels wrt nodes, given as a one- ot two-chars str combining: "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 degrees
• nodes_label_outline_width: width of the outline around node labels
• nodes_label_outline_color: color of the outline around node labels
• nodes_label_outline_palette: palette for nodes_label_outline_color
• nodes_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
• edges_draw_color, edges_draw_palette, edges_draw_style, and edges_draw_width: like nodes_draw_... but for edges (which means that information is taken from table edges if 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: like nodes_label... but for edges. Note that edges_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 (default 0.6) and cannot be a column/array of values
• edges_target_tip: shape of edge tip at target node, as listed in TableTipDesc.values. Values may be prefixed with "filled-" or "hollow-" to fill or not the tip drawing. TableTipDesc.alias provides short names for some edge tips.
• edges_target_color and edges_target_palette: color and palette of edge tips at target node
• edges_source_tip, edges_source_color, edges_source_palette: like edges_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_color and nodes_fill_color
• nodes_palette: nodes_draw_palette and nodes_fill_palette
• edges_tip_color: edges_target_color and edges_source_color
• edges_tip_palette: edges_target_palette and edges_source_palette
• edges_color: edges_draw_color and edges_tip_color
• edges_palette: edges_draw_palette and edges_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 list is a vbox, a vbox arranges its content into a ipywidget.VBox
• a list in a vbox arranges its content into an ipywidget.HBox
• a dict in a vbox arranges its content as an ipywidget.Accordion whose 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 of nodes and edges tables limited to the selected nodes and the edges connected to them. Options inspect_nodes and inspect_edges may 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.)