Class: StateMachineChecker::CTL::Implication

Inherits:

BinaryFormula

• Object
• Formula
• BinaryFormula
• StateMachineChecker::CTL::Implication

Defined in:

lib/state_machine_checker/ctl/implication.rb

Overview

Logical implication.

Instance Method Summary

• #check(model) ⇒ CheckResult
• #to_s ⇒ Object

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

Parameters:

• model (LabeledMachine)

Returns:

• (CheckResult)

# File 'lib/state_machine_checker/ctl/implication.rb', line 10

def check(model)
  subformula1.and(subformula2).or(Not.new(subformula1)).check(model)
end

#to_s ⇒ Object

# File 'lib/state_machine_checker/ctl/implication.rb', line 14

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