Class: StateMachineChecker::CTL::AU

Inherits:
BinaryFormula show all
Defined in:
lib/state_machine_checker/ctl/a_u.rb

Overview

The universal until operator.

Instance Method Summary collapse

Methods inherited from BinaryFormula

#atoms, #initialize

Methods inherited from Formula

#AU, #EU, #and, #implies, #or

Constructor Details

This class inherits a constructor from StateMachineChecker::CTL::BinaryFormula

Instance Method Details

#check(model) ⇒ CheckResult


12
13
14
15
16
# 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_sObject


18
19
20
# File 'lib/state_machine_checker/ctl/a_u.rb', line 18

def to_s
  "(#{subformula1}) AU (#{subformula2})"
end