Class: StateMachineChecker::CTL::AF

Inherits:

Object
Formula
UnaryOperator
StateMachineChecker::CTL::AF

Defined in:: lib/state_machine_checker/ctl/a_f.rb

Overview

The universal eventually operator.

Instance Method Summary collapse

Methods inherited from UnaryOperator

#atoms, #initialize

Methods inherited from Formula

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

Constructor Details

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

Instance Method Details

#check(model) ⇒ `CheckResult`

Parameters:

model (LabeledMachine)

Returns:

(CheckResult)



11
12
13

# File 'lib/state_machine_checker/ctl/a_f.rb', line 11

def check(model)
  Not.new(CTL::EG.new(Not.new(subformula))).check(model)
end

#to_s ⇒ `Object`



15
16
17

# File 'lib/state_machine_checker/ctl/a_f.rb', line 15

def to_s
  "AF(#{subformula})"
end