class StateMachineChecker::LabeledMachine

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

Attributes

fsm[R]
labeling[R]

Public Class Methods

new(fsm, labeling) click to toggle source

@param [FiniteStateMachine] fsm @param [Labeling] labeling

# File lib/state_machine_checker/labeled_machine.rb, line 7
def initialize(fsm, labeling)
  @fsm = fsm
  @labeling = labeling
end

Public Instance Methods

initial_state() click to toggle source

(see StateMachineChecker::FiniteStateMachine#initial_state)

# File lib/state_machine_checker/labeled_machine.rb, line 13
def initial_state
  fsm.initial_state
end
labels_for_state(state) click to toggle source

(see StateMachineChecker::Labeling#for_state)

# File lib/state_machine_checker/labeled_machine.rb, line 43
def labels_for_state(state)
  labeling.for_state(state)
end
states() click to toggle source

(see StateMachineChecker::FiniteStateMachine#states)

# File lib/state_machine_checker/labeled_machine.rb, line 23
def states
  fsm.states
end
transitions() click to toggle source

(see StateMachineChecker::FiniteStateMachine#transitions)

# File lib/state_machine_checker/labeled_machine.rb, line 18
def transitions
  fsm.transitions
end
transitions_from(state) click to toggle source

(see StateMachineChecker::FiniteStateMachine#transitions_from)

# File lib/state_machine_checker/labeled_machine.rb, line 38
def transitions_from(state)
  fsm.transitions_from(state)
end
transitions_to(state) click to toggle source

(see StateMachineChecker::FiniteStateMachine#transitions_to)

# File lib/state_machine_checker/labeled_machine.rb, line 33
def transitions_to(state)
  fsm.transitions_to(state)
end
traverse(from_state, reverse: false, &block) click to toggle source

(see StateMachineChecker::FiniteStateMachine#traverse)

# 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