class StateMachineChecker::CTL::Not

The logical negation of a formula.

Public Instance Methods

check(model) click to toggle source

Check whether each state is not satisfied by the subformula.

@param [LabeledMachine] model @return [CheckResult]

# 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_s() click to toggle source
# File lib/state_machine_checker/ctl/not.rb, line 31
def to_s
  "¬(#{subformula})"
end