Class: StateMachineChecker::CTL::EU

Inherits:
BinaryFormula show all
Defined in:
lib/state_machine_checker/ctl/e_u.rb

Overview

The existential until operator. This is the “strong” until, it is only satisfied if the second sub-formula is eventually satisifed.

Instance Method Summary collapse

Methods inherited from BinaryFormula

#atoms, #initialize

Methods inherited from Formula

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

Constructor Details

This class inherits a constructor from StateMachineChecker::CTL::BinaryFormula

Instance Method Details

#check(model) ⇒ CheckResult

Check which states of the model have a path for which the first subformula is satisifed until the second subformula is.

Parameters:

Returns:


13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
# File 'lib/state_machine_checker/ctl/e_u.rb', line 13

def check(model)
  subresult1 = subformula1.check(model)
  subresult2 = subformula2.check(model)

  result = subresult2.to_h # States satisfying sub-formula2 satisfy this.

  model.states.lazy.select { |s| subresult2.for_state(s).satisfied? }.each do |end_state|
    model.traverse(end_state, reverse: true) do |state, path|
      if state == end_state || subresult1.for_state(state).satisfied?
        # Don't update states that are already satisfied, to keep the
        # simpler witness.
        unless result[state].satisfied?
          result[state] = StateResult.new(true, path)
        end
        true
      else
        false
      end
    end
  end

  CheckResult.new(result)
end

#to_sObject


37
38
39
# File 'lib/state_machine_checker/ctl/e_u.rb', line 37

def to_s
  "(#{subformula1}) EU (#{subformula2})"
end