class StateMachineChecker::CTL::And
The logical conjunction of two or more sub-formulae.
Attributes
subformulae[R]
Public Class Methods
new(subformulae)
click to toggle source
Conjoin several formulae.
@param [Enumerator<Formula>] subformulae
@example
And.new([Atom.new(:even?), Atom.new(:positive?)])
# File lib/state_machine_checker/ctl/and.rb, line 13 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<Atom>]
# File lib/state_machine_checker/ctl/and.rb, line 20 def atoms subformulae.lazy.flat_map(&:atoms) end
check(model)
click to toggle source
Check which states of the model are satisfied by all subformulae.
@param [LabeledMachine] model @return [CheckResult]
# File lib/state_machine_checker/ctl/and.rb, line 28 def check(model) sub_results = subformulae.lazy.map { |f| f.check(model) } sub_results.reduce(&:intersection) end
to_s()
click to toggle source
# File lib/state_machine_checker/ctl/and.rb, line 33 def to_s subformulae.map(&:to_s).join(" ∧ ") end