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_state ⇒ Object

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

#states ⇒ Enumerator<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

#transitions ⇒ Object

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