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