class StateMachineChecker::CTL::EF
The existential eventually operator.
Public Instance Methods
check(model)
click to toggle source
Check which states of the model have as a successor a state satisfying the subformula.
@param [LabeledMachine] model @return [CheckResult]
# File lib/state_machine_checker/ctl/e_f.rb, line 12 def check(model) subresult = subformula.check(model) result = subresult.to_h model.states.each do |state| sub_state_result = subresult.for_state(state) if sub_state_result.satisfied? # Mark predecessors as satisfied. model.traverse(state, reverse: true) do |s, transitions| witness = transitions + sub_state_result.witness result[s] = StateResult.new(true, witness) end end end CheckResult.new(result) end
to_s()
click to toggle source
# File lib/state_machine_checker/ctl/e_f.rb, line 29 def to_s "EF(#{subformula})" end