Class: StateMachineChecker::CTL::Not

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

Overview

The logical negation of a formula.

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 whether each state is not satisfied by the subformula.

Parameters:

Returns:


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

def check(model)
  subresult = subformula.check(model)

  result = model.states.each_with_object({}) { |state, h|
    state_result = subresult.for_state(state)

    # Negate whether it was satisfied, keep the same path.
    path = if state_result.satisfied?
      state_result.witness
    else
      state_result.counterexample
    end
    h[state] = StateResult.new(!state_result.satisfied?, path)
  }

  CheckResult.new(result)
end

#to_sObject


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

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