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