Uses of Interface
dev.civl.mc.predicate.IF.CIVLStatePredicate
Packages that use CIVLStatePredicate
Package
Description
Module predicate defines predicates that are required to hold for any CIVL-C programs.
-
Uses of CIVLStatePredicate in dev.civl.mc.predicate.IF
Subinterfaces of CIVLStatePredicate in dev.civl.mc.predicate.IFModifier and TypeInterfaceDescriptioninterfaceThis represents a predicate in CNF, containing a number of predicates, called clauses, i.e., p1 & p2 & ...interfaceAn absolute deadlock occurs if all of the following hold: not every process has terminated no process has an enabled statement (note that a send statement is enabled iff the current number of buffered messages is less than the buffer bound).interfaceA functional equivalence predicate contains a specification output, which is a set of pairs (pathcondition, output variable map), and is checked at the final state of the program.interfaceAn potential deadlock occurs if all of the following hold: not every process has terminated the only enabled transitions are sends for which there is no matching receiveinterfaceMethods in dev.civl.mc.predicate.IF that return CIVLStatePredicateModifier and TypeMethodDescriptionAndPredicate.getUnreportedViolatedPredicate()Returns that predicate that has a violation that not yet been reported.Methods in dev.civl.mc.predicate.IF that return types with arguments of type CIVLStatePredicateModifier and TypeMethodDescriptionAndPredicate.clauses()Returns all predicates contained by this And predicate.Methods in dev.civl.mc.predicate.IF with parameters of type CIVLStatePredicateModifier and TypeMethodDescriptionvoidAndPredicate.addClause(CIVLStatePredicate predicate) Add a predicate as one clause of this And predicate.static AndPredicatePredicates.newAndPredicate(CIVLStatePredicate predicate)