Module dev.civl.mc
Package dev.civl.mc.predicate.IF
package dev.civl.mc.predicate.IF
Module predicate defines predicates that are required to hold for any CIVL-C programs.
-
ClassDescriptionThis represents a predicate in CNF, containing a number of predicates, called clauses, i.e., p1 & p2 & ...An 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).A 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.An 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 receive