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