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