Create a Finite Transition System from a tuple of fields.

Hint

To remember the arg order:

1) it starts with states (S0 requires S before it is defined)

2) continues with the pair (AP, L), because states are more fundamental than transitions (transitions require states to be defined) and because the state labeling L requires AP to be defined.

3) ends with the pair (Act, trans), because transitions in trans require actions in Act to be defined.

See Also

tuple2ba

Parameters:

• S (iterable of hashables) - set of states
• S0 (iterable of elements from S) - set of initial states, must be \subset S
• AP (iterable of hashables) - set of Atomic Propositions for state labeling: L: S-> 2^AP
• L (iterable of (state, AP_label) pairs: [(state0, {'p'} ), ...] | None, to skip state labeling.) - state labeling definition
• Act (iterable of hashables) - set of Actions for edge labeling: R: E-> Act
• trans (list of triples: [(from_state, to_state, act), ...] where act \in Act) - transition relation
• name (str) - used for file export

Return linear FTS with given labeling.

The resulting system will be a terminating sequence:

   s0-> s1-> ... -> sN

where: N = len(L) -1.

See Also

cycle_labeled_with

Parameters:

• L (iterable of state labels, e.g.,:

         [{'p', '!p', 'q',...]
  

  Single strings are identified with singleton Atomic Propositions, so [..., 'p',...] and [...,{'p'},...] are equivalent.

  ) - state labeling
• m (int) - starting index

Returns:

FTS with:

• states ['s0', ..., 'sN'], where N = len(L) -1
• state labels defined by L, so s0 is labeled with L[0], etc.
• transitions forming a sequence:
  • s_{i} ---> s_{i+1}, for: 0 <= i < N

Return cycle FTS with given labeling.

The resulting system will be a cycle:

   s0-> s1-> ... -> sN -> s0

where: N = len(L) -1.

See Also

line_labeled_with

Parameters:

• L (iterable of state labels, e.g., [{'p', 'q'}, ...] Single strings are identified with singleton Atomic Propositions, so [..., 'p',...] and [...,{'p'},...] are equivalent.) - state labeling

Returns:

FTS with:

• states ['s0', ..., 'sN'], where N = len(L) -1
• state labels defined by L, so s0 is labeled with L[0], etc.
• transitions forming a cycle:
  • s_{i} ---> s_{i+1}, for: 0 <= i < N
  • s_N ---> s_0

Make initial any state of ts labeled with any label in ap_labels.

For example if isinstance(ofts, FTS):

>>> from tulip.transys.transys import add_initial_states
>>> initial_labels = [{'home'}]
>>> add_initial_states(ofts, initial_labels)

Parameters:

• ap_labels (iterable of sets of elements from ts.atomic_propositions) - labels, each comprised of atomic propositions
• ts (FiniteTransitionSystem)