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