Class: StateMachineChecker::CTL::And

Inherits:
Formula
  • Object
show all
Defined in:
lib/state_machine_checker/ctl/and.rb

Overview

The logical conjunction of two or more sub-formulae.

Instance Method Summary collapse

Methods inherited from Formula

#AU, #EU, #and, #implies, #or

Constructor Details

#initialize(subformulae) ⇒ And

Conjoin several formulae.

Examples:

And.new([Atom.new(:even?), Atom.new(:positive?)])

13
14
15
# File 'lib/state_machine_checker/ctl/and.rb', line 13

def initialize(subformulae)
  @subformulae = subformulae
end

Instance Method Details

#atomsEnumerator<Atom>

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


20
21
22
# File 'lib/state_machine_checker/ctl/and.rb', line 20

def atoms
  subformulae.lazy.flat_map(&:atoms)
end

#check(model) ⇒ CheckResult

Check which states of the model are satisfied by all subformulae.


28
29
30
31
# 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_sObject


33
34
35
# File 'lib/state_machine_checker/ctl/and.rb', line 33

def to_s
  subformulae.map(&:to_s).join("")
end