class StateMachineChecker::CTL::Formula
Abstract base class for CTL
formulae.
Public Instance Methods
AU(end_formula)
click to toggle source
# 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)
click to toggle source
The existential until operator.
# 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
and(*other_subformulae)
click to toggle source
The logical conjuction of this formula with others.
# 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
implies(other_subformula)
click to toggle source
Logical implication
# 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)
click to toggle source
The logical disjunction of this formula with others.
# 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
Private Instance Methods
atom_or_formula(subformula)
click to toggle source
# File lib/state_machine_checker/ctl/formula.rb, line 33 def atom_or_formula(subformula) if subformula.is_a? Formula subformula else Atom.new(subformula) end end