class StateMachineChecker::CTL::AU

The universal until operator.

Public Instance Methods

check(model) click to toggle source

@param [LabeledMachine] model @return [CheckResult]

# File lib/state_machine_checker/ctl/a_u.rb, line 12
def check(model)
  Not.new(Not.new(subformula2).EU(Not.new(subformula1.or(subformula2)))
    .or(EG.new(Not.new(subformula2))))
    .check(model)
end
to_s() click to toggle source
# File lib/state_machine_checker/ctl/a_u.rb, line 18
def to_s
  "(#{subformula1}) AU (#{subformula2})"
end