Module dev.civl.gmc

Class Predicate

java.lang.Object
dev.civl.gmc.smc.Predicate
All Implemented Interfaces:
StatePredicateIF<Integer>

public class Predicate extends Object implements StatePredicateIF<Integer>
The predicate used for detecting violation state defined in the given list states.
  • Constructor Details

    • Predicate

      public Predicate(Integer... states)
  • Method Details

    • holdsAt

      public boolean holdsAt(Integer state)
      Does this predicate hold at the given state?

      For the Violation State Predicate, if the given state is in the field violationStates, this function will return true (which will make the SMC return false for this violation), else false.

      Specified by:
      holdsAt in interface StatePredicateIF<Integer>
      Parameters:
      state - any state in the state-transition system
      Returns:
      true iff this predicate holds at the state
    • explanation

      public String explanation()
      Description copied from interface: StatePredicateIF
      Returns a human-readable explanation of why the predicate does or does not hold, after method StatePredicateIF.holdsAt(S) has been called. The information returns should correspond to the last call to StatePredicateIF.holdsAt(S).
      Specified by:
      explanation in interface StatePredicateIF<Integer>
    • toString

      public String toString()
      Overrides:
      toString in class Object