Module: StateMachineChecker

Included in:
RspecMatchers::SatisfyMatcher
Defined in:
lib/state_machine_checker.rb,
lib/state_machine_checker/ctl/or.rb,
lib/state_machine_checker/ctl/a_f.rb,
lib/state_machine_checker/ctl/a_g.rb,
lib/state_machine_checker/ctl/a_u.rb,
lib/state_machine_checker/ctl/a_x.rb,
lib/state_machine_checker/ctl/and.rb,
lib/state_machine_checker/ctl/api.rb,
lib/state_machine_checker/ctl/e_f.rb,
lib/state_machine_checker/ctl/e_g.rb,
lib/state_machine_checker/ctl/e_u.rb,
lib/state_machine_checker/ctl/e_x.rb,
lib/state_machine_checker/ctl/not.rb,
lib/state_machine_checker/version.rb,
lib/state_machine_checker/ctl/atom.rb,
lib/state_machine_checker/labeling.rb,
lib/state_machine_checker/transition.rb,
lib/state_machine_checker/ctl/formula.rb,
lib/state_machine_checker/check_result.rb,
lib/state_machine_checker/state_result.rb,
lib/state_machine_checker/rspec_matchers.rb,
lib/state_machine_checker/ctl/implication.rb,
lib/state_machine_checker/labeled_machine.rb,
lib/state_machine_checker/ctl/binary_formula.rb,
lib/state_machine_checker/ctl/unary_operator.rb,
lib/state_machine_checker/finite_state_machine.rb,
lib/state_machine_checker/adapters/state_machines.rb

Overview

The main entrypoint is #check_satisfied. The other methods are provided primarily for debugging and transparency.

Defined Under Namespace

Modules: Adapters, CTL, RspecMatchers Classes: CheckResult, FiniteStateMachine, LabeledMachine, Labeling, StateResult, Transition

Constant Summary collapse

VERSION =
"0.1.0"

Instance Method Summary collapse

Instance Method Details

#build_labeled_machine(formula, instance_generator) ⇒ LabeledMachine

Build a labeled machine (Kripke structure) over the atomic propositions contained in the given formula.


33
34
35
36
37
38
39
40
41
42
# File 'lib/state_machine_checker.rb', line 33

def build_labeled_machine(formula, instance_generator)
  # TODO: Assumes state_machines gem.
  gem_machine = instance_generator.call.class.state_machine
  adapter = Adapters::StateMachines.new(gem_machine)
  fsm = FiniteStateMachine.new(adapter.initial_state, adapter.transitions)
  LabeledMachine.new(
    fsm,
    Labeling.new(formula.atoms, fsm, instance_generator)
  )
end

#check_satisfied(formula, instance_generator) ⇒ StateResult

Check whether a formula is satisfied by the state machine of a given class.


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

def check_satisfied(formula, instance_generator)
  labeled_machine = build_labeled_machine(formula, instance_generator)
  check = formula.check(labeled_machine)
  check.for_state(labeled_machine.initial_state)
end