Class: StateMachineChecker::LabeledMachine

Inherits:
Object
  • Object
show all
Defined in:
lib/state_machine_checker/labeled_machine.rb

Overview

A finite state machine where every node is mapped to a set of labels. AKA a Kripke structure.

Instance Method Summary collapse

Constructor Details

#initialize(fsm, labeling) ⇒ LabeledMachine

Returns a new instance of LabeledMachine.

Parameters:


7
8
9
10
# File 'lib/state_machine_checker/labeled_machine.rb', line 7

def initialize(fsm, labeling)
  @fsm = fsm
  @labeling = labeling
end

Instance Method Details

#initial_stateObject

Returns the value of attribute initial_state


13
14
15
# File 'lib/state_machine_checker/labeled_machine.rb', line 13

def initial_state
  fsm.initial_state
end

#labels_for_state(state) ⇒ Set<CTL::Atom>

Get the labels for the given state.

Parameters:

  • state (Symbol)

Returns:

  • (Set<CTL::Atom>)

    the atoms which are true in the state


43
44
45
# File 'lib/state_machine_checker/labeled_machine.rb', line 43

def labels_for_state(state)
  labeling.for_state(state)
end

#statesEnumerator<Symbol>

Enumerate the states.

Returns:

  • (Enumerator<Symbol>)

    an enumerator over the names of the states.


23
24
25
# File 'lib/state_machine_checker/labeled_machine.rb', line 23

def states
  fsm.states
end

#transitionsObject

Returns the value of attribute transitions


18
19
20
# File 'lib/state_machine_checker/labeled_machine.rb', line 18

def transitions
  fsm.transitions
end

#transitions_from(state) ⇒ Object


38
39
40
# File 'lib/state_machine_checker/labeled_machine.rb', line 38

def transitions_from(state)
  fsm.transitions_from(state)
end

#transitions_to(state) ⇒ Object


33
34
35
# File 'lib/state_machine_checker/labeled_machine.rb', line 33

def transitions_to(state)
  fsm.transitions_to(state)
end

#traverse(from_state, reverse: false) {|Symbol, Array<Symbol>| ... } ⇒ Object

Traverse the graph from the given state. Yield each state and the transitions from it to the from_state. If the result of the block is falsey for any state then the search will not continue to the children of that state.

Parameters:

  • from_state (Symbol)
  • reverse (true, false) (defaults to: false)

    traverse in reverse?

Yields:

  • (Symbol, Array<Symbol>)

28
29
30
# File 'lib/state_machine_checker/labeled_machine.rb', line 28

def traverse(from_state, reverse: false, &block)
  fsm.traverse(from_state, reverse: reverse, &block)
end