class StateMachineChecker::CTL::EX
The existential next operator.
Public Instance Methods
check(model)
click to toggle source
Check which states of the model have as a direct successor a state satisfying the subformula.
@param [LabeledMachine] model @return [CheckResult]
# 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_s()
click to toggle source
# File lib/state_machine_checker/ctl/e_x.rb, line 35 def to_s "EX(#{subformula})" end