class StateMachineChecker::CTL::EU
The existential until operator. This is the “strong” until, it is only satisfied if the second sub-formula is eventually satisifed.
Public Instance Methods
check(model)
click to toggle source
Check which states of the model have a path for which the first subformula is satisifed until the second subformula is.
@param [LabeledMachine] model @return [CheckResult]
# File lib/state_machine_checker/ctl/e_u.rb, line 13 def check(model) subresult1 = subformula1.check(model) subresult2 = subformula2.check(model) result = subresult2.to_h # States satisfying sub-formula2 satisfy this. model.states.lazy.select { |s| subresult2.for_state(s).satisfied? }.each do |end_state| model.traverse(end_state, reverse: true) do |state, path| if state == end_state || subresult1.for_state(state).satisfied? # Don't update states that are already satisfied, to keep the # simpler witness. unless result[state].satisfied? result[state] = StateResult.new(true, path) end true else false end end end CheckResult.new(result) end
to_s()
click to toggle source
# File lib/state_machine_checker/ctl/e_u.rb, line 37 def to_s "(#{subformula1}) EU (#{subformula2})" end