class StateMachineChecker::Labeling

A mapping from states to the values of each atom.

Attributes

labels_by_state[R]

Public Class Methods

new(atoms, machine, instance_generator) click to toggle source

@param [Enumerator<CTL::Atom>] atoms the atoms which will be the labels. @param [FiniteStateMachine] machine the machine to generate labels for. @param [Proc] instance_generator a nullary function which returns an

instance of an object in the initial state.
# File lib/state_machine_checker/labeling.rb, line 8
def initialize(atoms, machine, instance_generator)
  @labels_by_state = build_map(atoms, machine, instance_generator)
end

Public Instance Methods

for_state(state) click to toggle source

Get the labels for the given state.

@param [Symbol] state @return [Set<CTL::Atom>] the atoms which are true in the state

# File lib/state_machine_checker/labeling.rb, line 16
def for_state(state)
  labels_by_state[state]
end

Private Instance Methods

build_map(atoms, machine, instance_generator) click to toggle source

Generate a hash of state -> atoms

# File lib/state_machine_checker/labeling.rb, line 25
def build_map(atoms, machine, instance_generator)
  machine.state_paths.each_with_object({}) { |(state, transitions), states_map|
    instance = instance_from_transitions(transitions, instance_generator)

    states_map[state] = atoms.each_with_object(Set.new) { |atom, labels|
      if atom.apply(instance)
        labels << atom
      end
    }
  }
end
instance_from_transitions(transitions, instance_generator) click to toggle source

Walk an instance through the given transitions.

# File lib/state_machine_checker/labeling.rb, line 38
def instance_from_transitions(transitions, instance_generator)
  instance = instance_generator.call

  transitions.each do |transition|
    transition.execute(instance)
  end

  instance
end