Class: StateMachineChecker::CTL::Formula

Inherits:
Object
  • Object
show all
Defined in:
lib/state_machine_checker/ctl/formula.rb

Overview

Abstract base class for CTL formulae.

Direct Known Subclasses

And, Atom, BinaryFormula, Or, UnaryOperator

Instance Method Summary collapse

Instance Method Details

#and(*other_subformulae) ⇒ Object

The logical conjuction of this formula with others.


6
7
8
9
# File 'lib/state_machine_checker/ctl/formula.rb', line 6

def and(*other_subformulae)
  other_subformulae.map! { |f| atom_or_formula(f) }
  And.new(other_subformulae << self)
end

#AU(end_formula) ⇒ Object

rubocop:disable Naming/MethodName


27
28
29
# File 'lib/state_machine_checker/ctl/formula.rb', line 27

def AU(end_formula) # rubocop:disable Naming/MethodName
  AU.new(self, atom_or_formula(end_formula))
end

#EU(end_formula) ⇒ Object

The existential until operator.


23
24
25
# File 'lib/state_machine_checker/ctl/formula.rb', line 23

def EU(end_formula) # rubocop:disable Naming/MethodName
  EU.new(self, atom_or_formula(end_formula))
end

#implies(other_subformula) ⇒ Object

Logical implication


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

def implies(other_subformula)
  Implication.new(self, atom_or_formula(other_subformula))
end

#or(*other_subformulae) ⇒ Object

The logical disjunction of this formula with others.


12
13
14
15
# File 'lib/state_machine_checker/ctl/formula.rb', line 12

def or(*other_subformulae)
  other_subformulae.map! { |f| atom_or_formula(f) }
  Or.new(other_subformulae << self)
end