Module dev.civl.gmc
Package dev.civl.gmc

Interface StatePredicateIF<S>

Type Parameters:
S - the type used to represent states
All Known Implementing Classes:
FalsePredicate, Predicate
public interface StatePredicateIF<S>
A state predicate is basically a function which returns either true or false at any state in the transition system. It is typically used to encode a "bad" property, such as deadlock.

  • Method Summary

    Modifier and Type
    Method
    Description
    String
    explanation()
    Returns a human-readable explanation of why the predicate does or does not hold, after method holdsAt(S) has been called.
    boolean
    holdsAt(S state)
    Does this predicate hold at the given state?

  • Method Details

    • holdsAt

      boolean holdsAt(S state)
      Does this predicate hold at the given state?
      Parameters:
      state - any state in the state-transition system
      Returns:
      true iff this predicate holds at the state

    • explanation

      String explanation()
      Returns a human-readable explanation of why the predicate does or does not hold, after method holdsAt(S) has been called. The information returns should correspond to the last call to holdsAt(S).