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