Class: StateMachineChecker::CTL::EG

Inherits:
UnaryOperator show all
Defined in:
lib/state_machine_checker/ctl/e_g.rb

Overview

The existential universal operator.

Instance Method Summary collapse

Methods inherited from UnaryOperator

#atoms, #initialize

Methods inherited from Formula

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

Constructor Details

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

Instance Method Details

#check(model) ⇒ CheckResult

Check which states of the model have a path for which the subformula is always satisfied

Parameters:

Returns:



10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
 
# File 'lib/state_machine_checker/ctl/e_g.rb', line 10

def check(model)
  subresult = subformula.check(model)
  projection = subformula_projection(model, subresult)
  scc = strongly_connected_components(projection)

  # Components must have more than one element, a self loop, or no
  # transitions in the original fsm.
  # TODO: this being necessary probably means we're doing something wrong.
  scc.select! do |states|
    states.length > 1 ||
      begin
        c = states.first
        transitions = model.transitions_from(c)

        transitions.empty? ||
          transitions.any? { |t| t.to == c }
      end
  end

  build_check_result(scc, model, projection)
end

#to_s ⇒ Object 



32
33
34
 
# File 'lib/state_machine_checker/ctl/e_g.rb', line 32

def to_s
  "EG(#{subformula})"
end