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