class StateMachineChecker::CTL::Or

The logical disjunction of two or more sub-formulae.

Attributes

subformulae[R]

Public Class Methods

new(subformulae) click to toggle source

Disjoin several formulae.

@example

Or.new([Atom.new(:even?), Atom.new(:positive?)])
# File lib/state_machine_checker/ctl/or.rb, line 11
def initialize(subformulae)
  @subformulae = subformulae
end

Public Instance Methods

atoms() click to toggle source

Return an enumerator over the atoms of all sub-formulae.

@return [Enumerator]

# File lib/state_machine_checker/ctl/or.rb, line 18
def atoms
  subformulae.lazy.flat_map(&:atoms)
end
check(model) click to toggle source

Check which states of the model are satisfied by at least one subformulae.

@param [LabeledMachine] model @return [CheckResult]

# File lib/state_machine_checker/ctl/or.rb, line 26
def check(model)
  sub_results = subformulae.lazy.map { |f| f.check(model) }
  sub_results.reduce(&:union)
end
to_s() click to toggle source
# File lib/state_machine_checker/ctl/or.rb, line 31
def to_s
  subformulae.map(&:to_s).map { |s| "(#{s})" }.join(" ∨ ")
end