Class: StateMachineChecker::CTL::EX

Inherits:
UnaryOperator show all
Defined in:
lib/state_machine_checker/ctl/e_x.rb

Overview

The existential next operator.

Instance Method Summary collapse

Methods inherited from UnaryOperator

#atoms, #initialize

Methods inherited from Formula

#AU, #EU, #and, #implies, #or

Constructor Details

This class inherits a constructor from StateMachineChecker::CTL::UnaryOperator

Instance Method Details

#check(model) ⇒ CheckResult

Check which states of the model have as a direct successor a state satisfying the subformula.


14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
# File 'lib/state_machine_checker/ctl/e_x.rb', line 14

def check(model)
  # Initialize hash with every state unsatisfied.
  result = model.states.each_with_object({}) { |s, h|
    h[s] = StateResult.new(false, [])
  }

  subresult = subformula.check(model)
  model.states.each do |state|
    sub_state_result = subresult.for_state(state)

    if sub_state_result.satisfied? # Mark direct predecessors as satisfied.
      model.transitions_to(state).each do |transition|
        witness = [transition.name] + sub_state_result.witness
        result[transition.from] = StateResult.new(true, witness)
      end
    end
  end

  CheckResult.new(result)
end

#to_sObject


35
36
37
# File 'lib/state_machine_checker/ctl/e_x.rb', line 35

def to_s
  "EX(#{subformula})"
end