Class: StateMachineChecker::CTL::Or

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

Overview

The logical disjunction of two or more sub-formulae.

Instance Method Summary collapse

Methods inherited from Formula

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

Constructor Details

#initialize(subformulae) ⇒ Or

Disjoin several formulae.

Examples:

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

11
12
13
# File 'lib/state_machine_checker/ctl/or.rb', line 11

def initialize(subformulae)
  @subformulae = subformulae
end

Instance Method Details

#atomsEnumerator

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

Returns:

  • (Enumerator)

18
19
20
# File 'lib/state_machine_checker/ctl/or.rb', line 18

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

#check(model) ⇒ CheckResult

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

Parameters:

Returns:


26
27
28
29
# 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_sObject


31
32
33
# File 'lib/state_machine_checker/ctl/or.rb', line 31

def to_s
  subformulae.map(&:to_s).map { |s| "(#{s})" }.join("")
end