Initialize States.

Parameters:

• graph (LabeledDiGraph)

Overrides: object.__init__

Return list of states.

For more details see LabeledDiGraph.nodes

str(x)

Overrides: object.__str__

(inherited documentation)

Wraps LabeledDiGraph.add_node,

which wraps networkx.MultiDiGraph.add_node.

Wraps LabeledDiGraph.add_nodes_from,

which wraps networkx.MultiDiGraph.add_nodes_from.

Remove state from states (including initial).

Wraps networkx.MultiDiGraph.remove_node.

Remove a list of states.

Iterates States.remove to imitate networkx.MultiDiGraph.remove_nodes_from, handling also initial states.

Direct successor set (1-hop) for given states.

Edge labels are ignored.

If multiple states provided, then union Post(s) for s in states provided.

See Also

• pre
• Def. 2.3, p.23 [BK08]

Parameters:

• states -
  • None, so initial states returned
  • single state or
  • set of states or

Returns: set

Return direct predecessors (1-hop) of given state.

See Also

• post
• Def. 2.3, p.23 [BK08]

Returns: set

Return states reachable from given state.

Iterated post(), a wrapper of networkx.descendants.

Return states from which the given state can be reached.

A wrapper of networkx.ancestors.

Color the given state.

The state is filled with given color, rendered with dot when plotting and saving.

Parameters:

• state - valid system state
• color (str of valid dot color) - with which to paint state

Filter by desired states and by desired state labels.

Examples

Assume that the system is:

>>> import transys as trs
>>> ts = trs.FTS()
>>> ts.atomic_propositions.add('p')
>>> ts.states.add('s0', ap={'p'})

• To find the label of a single state 's0':

  >>> a = ts.states.find(['s0'] )
  >>> (s0_, label) = a[0]
  >>> print(label)
  {'ap': set(['p'])}

• To find all states with a specific label {'p'}:

  >>> ts.states.add('s1', ap={'p'})
  >>> b = ts.states.find(with_attr_dict={'ap':{'p'} } )
  >>> states = [state for (state, label_) in b]
  >>> print(set(states) )
  {'s0', 's1'}

• To find all states in subset M labeled with {'p'}:

  >>> ts.states.add('s2', ap={'p'})
  >>> M = {'s0', 's2'}
  >>> b = ts.states.find(M, {'ap': {'p'} } )
  >>> states = [state for (state, label_) in b]
  >>> print(set(states) )
  {'s0', 's2'}

Parameters:

• states ('any' (default) | iterable of valid states | single valid state) - subset of states over which to search
• with_attr_dict ({sublabel_type : desired_sublabel_value, ...} | leave empty, to allow any state label (default)) - label with which to filter the states
• with_attr - label key-value pairs which take precedence over with_attr_dict.

Returns: list of labeled states

[(state, label),...] where:

• state \in states
• label: dict

Return True if state has no outgoing transitions.

See Also

Def. 2.4, p.23 [BK08]

initial

Return SubSet of initial states.

Get Method:

unreachable.initial(self) - Return SubSet of initial states.

Set Method:

unreachable.initial(self, states)