/**CFile***********************************************************************
FileName [ctlpUtil.c]
PackageName [ctlp]
Synopsis [Routines for manipulating CTL formulas.]
Description [This file contains routines for accessing the fields of the CTL
formula data structure, for printing CTL formulas, for reading CTL formulas
from a file, and for converting formulas to the existential form.]
Remarks [There are two types of conversion routines. One set, for
mc and amc, converts a formula to existential normal form, i.e. the
AX, AU and AG operators are converted. The other set, used in imc,
converts to simple existential form, a form consisting only of
E-operators and the boolean operators AND and NOT.
Simple existential form is incompatible with the mc debug routines,
because these depend on the specific form of the converted formula
to decide what the original formula was.
In the long run, the existential form should probably go, and the
debug routines should be adapted. The only drawback of simple
existential form is that the XOR gets expanded into three nontrivial
operations, so maybe XOR (or IFF) should be retained. (RB.)]
Author [Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto,
Jae-Young Jang, In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
All rights reserved.
Permission is hereby granted, without written agreement and without license
or royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
"AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
******************************************************************************/
#include "ctlpInt.h"
#include "errno.h"
static char rcsid[] UNUSED = "$Id: ctlpUtil.c,v 1.71 2009/04/11 18:25:53 fabio Exp $";
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
/**Variable********************************************************************
Synopsis [Array of CTL formulas (Ctlp_Formula_t) read from a file.]
SeeAlso [Ctlp_FormulaArrayFree]
******************************************************************************/
static array_t *globalFormulaArray;
static int changeBracket = 1;
/* see ctlpInt.h for documentation */
int CtlpGlobalError;
Ctlp_Formula_t *CtlpGlobalFormula;
st_table *CtlpMacroTable;
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static Ctlp_Formula_t * FormulaCreateWithType(Ctlp_FormulaType type);
static int FormulaCompare(const char *key1, const char *key2);
static int FormulaHash(char *key, int modulus);
static Ctlp_Formula_t * FormulaHashIntoUniqueTable(Ctlp_Formula_t *formula, st_table *uniqueTable);
static Ctlp_Formula_t * FormulaConvertToExistentialDAG(Ctlp_Formula_t *formula);
static void FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue);
static void FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula, Ctlp_Formula_t *parent, int compareValue);
static int FormulaGetCompareValue(Ctlp_Formula_t *formula);
static int FormulaIsConvertible(Ctlp_Formula_t *formula);
static Ctlp_Formula_t * ReplaceSimpleFormula(Ctlp_Formula_t *formula);
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Parses a file containing a set of CTL formulas.]
Description [Parses a file containing a set of semicolon-ending CTL
formulas, and returns an array of Ctlp_Formula_t representing those
formulas. If an error is detected while parsing the file, the routine frees
any allocated memory and returns NULL.]
SideEffects [Manipulates the global variables globalFormulaArray,
CtlpGlobalError and CtlpGlobalFormula.]
SeeAlso [Ctlp_FormulaArrayFree Ctlp_FormulaPrint]
******************************************************************************/
array_t *
Ctlp_FileParseFormulaArray(
FILE * fp)
{
st_generator *stGen;
char *name;
Ctlp_Formula_t *formula;
char *flagValue;
/*
* Initialize the global variables.
*/
globalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
CtlpGlobalError = 0;
CtlpGlobalFormula = NIL(Ctlp_Formula_t);
CtlpMacroTable = st_init_table(strcmp,st_strhash);
CtlpFileSetup(fp);
/*
* Check if changing "[] -> <>" is disabled.
*/
flagValue = Cmd_FlagReadByName("ctl_change_bracket");
if (flagValue != NIL(char)) {
if (strcmp(flagValue, "yes") == 0)
changeBracket = 1;
else if (strcmp(flagValue, "no") == 0)
changeBracket = 0;
else {
fprintf(vis_stderr,
"** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n",
flagValue);
}
}
(void)CtlpYyparse();
st_foreach_item(CtlpMacroTable,stGen,&name,&formula){
FREE(name);
CtlpFormulaFree(formula);
}
st_free_table(CtlpMacroTable);
/*
* Clean up if there was an error, otherwise return the array.
*/
if (CtlpGlobalError){
Ctlp_FormulaArrayFree(globalFormulaArray);
return NIL(array_t);
}
else {
return globalFormulaArray;
}
}
/**Function********************************************************************
Synopsis [Returns formula as a character string.]
Description [Returns formula as a character string. All subformulas are
delimited by parenthesis. The syntax used is the same as used by the CTL
parser. Does nothing if passed a NULL formula.]
SideEffects []
******************************************************************************/
char *
Ctlp_FormulaConvertToString(
Ctlp_Formula_t * formula)
{
char *s1 = NIL(char);
char *s2 = NIL(char);
char *tmpString = NIL(char);
char *result;
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(char);
}
/* The formula is a leaf. */
if (formula->type == Ctlp_ID_c){
return util_strcat3((char *)(formula->left), "=",(char *)(formula->right));
}
/* If the formula is a non-leaf, the function is called recursively */
s1 = Ctlp_FormulaConvertToString(formula->left);
s2 = Ctlp_FormulaConvertToString(formula->right);
switch(formula->type) {
/*
* The cases are listed in rough order of their expected frequency.
*/
case Ctlp_OR_c:
tmpString = util_strcat3(s1, " + ",s2);
result = util_strcat3("(", tmpString, ")");
break;
case Ctlp_AND_c:
tmpString = util_strcat3(s1, " * ", s2);
result = util_strcat3("(", tmpString, ")");
break;
case Ctlp_THEN_c:
tmpString = util_strcat3(s1, " -> ", s2);
result = util_strcat3("(", tmpString, ")");
break;
case Ctlp_XOR_c:
tmpString = util_strcat3(s1, " ^ ", s2);
result = util_strcat3("(", tmpString, ")");
break;
case Ctlp_EQ_c:
tmpString = util_strcat3(s1, " <-> ", s2);
result = util_strcat3("(", tmpString, ")");
break;
case Ctlp_NOT_c:
tmpString = util_strcat3("(", s1, ")");
result = util_strcat3("!", tmpString, "");
break;
case Ctlp_EX_c:
result = util_strcat3("EX(", s1, ")");
FREE(s1);
break;
case Ctlp_EG_c:
result = util_strcat3("EG(", s1, ")");
break;
case Ctlp_EF_c:
result = util_strcat3("EF(", s1, ")");
break;
case Ctlp_EU_c:
tmpString = util_strcat3("E(", s1, " U ");
result = util_strcat3(tmpString, s2, ")");
break;
case Ctlp_AX_c:
result = util_strcat3("AX(", s1, ")");
break;
case Ctlp_AG_c:
result = util_strcat3("AG(", s1, ")");
break;
case Ctlp_AF_c:
result = util_strcat3("AF(", s1, ")");
break;
case Ctlp_AU_c:
tmpString = util_strcat3("A(", s1, " U ");
result = util_strcat3(tmpString, s2, ")");
break;
case Ctlp_TRUE_c:
result = util_strsav("TRUE");
break;
case Ctlp_FALSE_c:
result = util_strsav("FALSE");
break;
case Ctlp_Init_c:
result = util_strsav("Init");
break;
case Ctlp_Cmp_c:
if (formula->compareValue == 0)
tmpString = util_strcat3("[", s1, "] = ");
else
tmpString = util_strcat3("[", s1, "] != ");
result = util_strcat3(tmpString, s2, "");
break;
case Ctlp_FwdU_c:
tmpString = util_strcat3("FwdU(", s1, ",");
result = util_strcat3(tmpString, s2, ")");
break;
case Ctlp_FwdG_c:
tmpString = util_strcat3("FwdG(", s1, ",");
result = util_strcat3(tmpString, s2, ")");
break;
case Ctlp_EY_c:
result = util_strcat3("EY(", s1, ")");
break;
default:
fail("Unexpected type");
}
if (s1 != NIL(char)) {
FREE(s1);
}
if (s2 != NIL(char)) {
FREE(s2);
}
if (tmpString != NIL(char)) {
FREE(tmpString);
}
return result;
}
/**Function********************************************************************
Synopsis [Prints a formula to a file.]
Description [Prints a formula to a file. All subformulas are delimited by
parenthesis. The syntax used is the same as used by the CTL parser. Does
nothing if passed a NULL formula.]
SideEffects []
******************************************************************************/
void
Ctlp_FormulaPrint(
FILE * fp,
Ctlp_Formula_t * formula)
{
char *tmpString;
if (formula == NIL(Ctlp_Formula_t)) {
return;
}
tmpString = Ctlp_FormulaConvertToString(formula);
(void) fprintf(fp, "%s", tmpString);
FREE(tmpString);
}
/**Function********************************************************************
Synopsis [Gets the type of a formula.]
Description [Gets the type of a formula. See ctlp.h for all the types. It is
an error to call this function on a NULL formula.]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_FormulaType
Ctlp_FormulaReadType(
Ctlp_Formula_t * formula)
{
assert( formula != NIL(Ctlp_Formula_t) );
return (formula->type);
}
#if 0
boolean
Ctlp_FormulaReadEvenNegations(
Ctlp_Formula_t * formula)
{
assert(formula != NIL(Ctlp_Formula_t));
return (formula->even_negations);
}
#endif
/**Function********************************************************************
Synopsis [Gets the compare value of a formula.]
Description [Gets the compare value of a formula. It is an error to call
this function on a NULL formula.]
SideEffects []
SeeAlso []
******************************************************************************/
int
Ctlp_FormulaReadCompareValue(
Ctlp_Formula_t * formula)
{
int value;
assert( formula != NIL(Ctlp_Formula_t));
value = formula->compareValue;
return (value);
}
/**Function********************************************************************
Synopsis [Reads the variable name of a leaf formula.]
Description [Reads the variable name of a leaf formula.
It is an error to call this function on a non-leaf formula.]
SideEffects []
******************************************************************************/
char *
Ctlp_FormulaReadVariableName(
Ctlp_Formula_t * formula)
{
if (formula->type != Ctlp_ID_c){
fail("Ctlp_FormulaReadVariableName() was called on a non-leaf formula.");
}
return ((char *)(formula->left));
}
/**Function********************************************************************
Synopsis [Reads the value name of a leaf formula.]
Description [Reads the value name of a leaf formula.
It is an error to call this function on a non-leaf formula.]
SideEffects []
******************************************************************************/
char *
Ctlp_FormulaReadValueName(
Ctlp_Formula_t * formula)
{
if (formula->type != Ctlp_ID_c){
fail("Ctlp_FormulaReadValueName() was called on a non-leaf formula.");
}
return ((char *)(formula->right));
}
/**Function********************************************************************
Synopsis [Gets the left child of a formula.]
Description [Gets the left child of a formula. User must not free this
formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
SideEffects []
SeeAlso [Ctlp_FormulaReadRightChild]
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaReadLeftChild(
Ctlp_Formula_t * formula)
{
if (formula->type != Ctlp_ID_c){
return (formula->left);
}
return NIL(Ctlp_Formula_t);
}
/**Function********************************************************************
Synopsis [Gets the right child of a formula.]
Description [Gets the right child of a formula. User must not free this
formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
SideEffects []
SeeAlso [Ctlp_FormulaReadLeftChild]
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaReadRightChild(
Ctlp_Formula_t * formula)
{
if (formula->type != Ctlp_ID_c){
return (formula->right);
}
return NIL(Ctlp_Formula_t);
}
/**Function********************************************************************
Synopsis [Gets a copy of the set of states for which this formula is
true.]
Description [Gets a copy of the MDD representing the set of states for which
this formula is true. It is the user's responsibility to free this MDD. If
the set of states has not yet been computed, then a NULL mdd_t is
returned. It is an error to call this function on a NULL formula.]
SideEffects []
SeeAlso [Ctlp_FormulaSetStates]
******************************************************************************/
mdd_t *
Ctlp_FormulaObtainStates(
Ctlp_Formula_t * formula)
{
assert(formula != NIL(Ctlp_Formula_t));
if (formula->states == NIL(mdd_t) ||
formula->latest == Ctlp_Incomparable_c) {
return NIL(mdd_t);
}
else {
return mdd_dup(formula->states);
}
}
/**Function********************************************************************
Synopsis [Stores the set of states with the formula.]
Description [Stores the MDD with the formula (a copy is not made,
and hence, the caller should not later free this MDD). This MDD is
intended to represent the set of states for which the formula is
true. It is an error to call this function on a NULL formula.]
SideEffects []
SeeAlso [Ctlp_FormulaObtainStates]
******************************************************************************/
void
Ctlp_FormulaSetStates(
Ctlp_Formula_t * formula,
mdd_t * states)
{
assert(formula != NIL(Ctlp_Formula_t));
/* RB: added the next two lines. Given the Description, this was a
bug */
if(formula->states != NIL(mdd_t))
mdd_free(formula->states);
formula->states = states;
formula->latest = Ctlp_Exact_c;
}
/**Function********************************************************************
Synopsis [Gets (a copy of) the latest approximation of the satisfying set]
Description [Gets the satisfying set or an approximation of it. The most
recently computed approximation is returned. If the
exact set is available, it will return that, because it is never superseded.
If neither exact nor approximate satisfying set is available, or
approx is Ctlp_Incomparable_c, it fails.]
SideEffects []
SeeAlso [Ctlp_FormulaSetApproxStates]
******************************************************************************/
mdd_t *
Ctlp_FormulaObtainLatestApprox(
Ctlp_Formula_t *formula)
{
if (formula->latest == Ctlp_Exact_c)
return mdd_dup(formula->states);
if (formula->latest == Ctlp_Overapprox_c)
return mdd_dup(formula->overapprox);
if (formula->latest == Ctlp_Underapprox_c)
return mdd_dup(formula->underapprox);
if (formula->latest == Ctlp_Incomparable_c)
return mdd_dup(formula->states);
assert(0); /* we should never get here */
return NIL(mdd_t);
}
/**Function********************************************************************
Synopsis [Gets (a copy of) an approximation of the satisfying set]
Description [Gets the required approximation of the satisfying set. If the
exact set is available, it will return that. If neither is available, or
approx is Ctlp_Incomparable_c, it will return NULL.]
SideEffects []
SeeAlso [Ctlp_FormulaSetApproxStates]
******************************************************************************/
mdd_t *
Ctlp_FormulaObtainApproxStates(
Ctlp_Formula_t *formula,
Ctlp_Approx_t approx)
{
if(approx == Ctlp_Incomparable_c)
return NIL(mdd_t);
if (formula->states != NIL(mdd_t))
return mdd_dup(formula->states);
if(approx == Ctlp_Exact_c)
return NIL(mdd_t);
if(approx == Ctlp_Overapprox_c){
if(formula->overapprox == NIL(mdd_t))
return NIL(mdd_t);
else
return mdd_dup(formula->overapprox);
}
if(approx == Ctlp_Underapprox_c){
if(formula->underapprox == NIL(mdd_t))
return NIL(mdd_t);
else
return mdd_dup(formula->underapprox);
}
assert(0); /* we should never get here */
return NIL(mdd_t);
}
/**Function********************************************************************
Synopsis [Stores (an approximation of) the set of states with the
formula.]
Description [Sets the set of states or an under or overapproximation
thereof, depending on the approx flag. If there is already an under
or overapproximation, it is overwritten. If the exact set is given,
the approx fields are cleared. Setting an incomparable
approximation results in no action being taken. An approximation
does not replace the exact set. A copy of the mdd is not made, so
the caller should not free it.]
SideEffects []
SeeAlso [Ctlp_FormulaObtainApproxStates Ctlp_FormulaObtainLatestApprox]
******************************************************************************/
void
Ctlp_FormulaSetApproxStates(
Ctlp_Formula_t * formula,
mdd_t * states,
Ctlp_Approx_t approx)
{
if (formula->latest == Ctlp_Exact_c) {
mdd_free(states);
return;
}
formula->latest = approx;
if (approx == Ctlp_Exact_c) {
if (formula->states != NIL(mdd_t))
mdd_free(formula->states);
formula->states = states;
if (formula->underapprox != NIL(mdd_t)) {
mdd_free(formula->underapprox);
formula->underapprox = NIL(mdd_t);
}
if (formula->overapprox != NIL(mdd_t)) {
mdd_free(formula->overapprox);
formula->overapprox = NIL(mdd_t);
}
return;
}
if (approx == Ctlp_Underapprox_c) {
/* you could perform a union instead, but typical use will
have monotonically increasing underapproximations */
if(formula->underapprox != NIL(mdd_t))
mdd_free(formula->underapprox);
formula->underapprox = states;
}
if (approx == Ctlp_Overapprox_c) {
/* you could perform an intersection instead */
if (formula->overapprox != NIL(mdd_t))
mdd_free(formula->overapprox);
formula->overapprox = states;
}
/* This case is possible; for instance when both children of an implication
* with (All, S) condition are underapproximated. We may lose some states
* from the left if they are not in S. These cause an overapproximation.
* We may also lose some states from the right. These cause an
* underapproximation. When the two effects are combined, we get something
* incomparable, yet sufficient to produce the exact result, because it is
* accurate over S. */
if (approx == Ctlp_Incomparable_c) {
if (formula->states != NIL(mdd_t))
mdd_free(formula->states);
formula->states = states;
}
return;
}
/**Function********************************************************************
Synopsis [Sets the debug information of a formula.]
Description [Sets the debug information of a CTL formula. The data is
uninterpreted. FreeFn is a pointer to a function that takes a formula as
input and returns void. FreeFn should free all the memory associated with
the debug data; it is called when this formula is freed.]
SideEffects []
SeeAlso [Ctlp_FormulaReadDebugData]
******************************************************************************/
void
Ctlp_FormulaSetDbgInfo(
Ctlp_Formula_t * formula,
void *data,
Ctlp_DbgInfoFreeFn freeFn)
{
if (formula->dbgInfo.data != NIL(void)){
assert(formula->dbgInfo.freeFn != NULL);
(*formula->dbgInfo.freeFn)(formula);
}
formula->dbgInfo.data = data;
formula->dbgInfo.freeFn = freeFn;
}
/**Function********************************************************************
Synopsis [Returns the debug data associated with a formula.]
Description [Returns the debug data associated with a formula. These data
are uninterpreted by the ctlp package.]
SideEffects []
SeeAlso [Ctlp_FormulaSetDbgInfo]
******************************************************************************/
void *
Ctlp_FormulaReadDebugData(
Ctlp_Formula_t * formula)
{
return formula->dbgInfo.data;
}
/**Function********************************************************************
Synopsis [Returns TRUE if formula was converted, else FALSE.]
from AX/AG/AU/AF]
Description [Returns TRUE if formula was converted from a formula of type
AG, AX, AU, AF, or EF via a call to
Ctlp_FormulaConvertToExistentialFormTree or
Ctlp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.]
SideEffects []
******************************************************************************/
boolean
Ctlp_FormulaTestIsConverted(
Ctlp_Formula_t * formula)
{
return formula->dbgInfo.convertedFlag;
}
/**Function********************************************************************
Synopsis [Returns TRUE if formula contains no path quantifiers.]
Description [Test if a CTL formula has any path quantifiers in it;
if so return false, else true. For a CTL formula, being quantifier-free
and being propositional are equivalent.]
SideEffects []
******************************************************************************/
boolean
Ctlp_FormulaTestIsQuantifierFree(
Ctlp_Formula_t *formula)
{
boolean lCheck;
boolean rCheck;
Ctlp_Formula_t *leftChild;
Ctlp_Formula_t *rightChild;
Ctlp_FormulaType type;
if ( formula == NIL( Ctlp_Formula_t ) ) {
return TRUE;
}
type = Ctlp_FormulaReadType( formula );
if ( ( type == Ctlp_ID_c ) ||
( type == Ctlp_TRUE_c ) ||
( type == Ctlp_FALSE_c ) ) {
return TRUE;
}
if ( ( type != Ctlp_OR_c ) &&
( type != Ctlp_AND_c ) &&
( type != Ctlp_NOT_c ) &&
( type != Ctlp_THEN_c ) &&
( type != Ctlp_XOR_c ) &&
( type != Ctlp_EQ_c ) ) {
return FALSE;
}
leftChild = Ctlp_FormulaReadLeftChild( formula );
lCheck = Ctlp_FormulaTestIsQuantifierFree( leftChild );
if (lCheck == FALSE)
return FALSE;
rightChild = Ctlp_FormulaReadRightChild( formula );
rCheck = Ctlp_FormulaTestIsQuantifierFree( rightChild );
return rCheck;
}
/**Function********************************************************************
Synopsis [Annotates the each node in parse tree with its negation
parity.]
Description [This function must be called at the top level with
parity = Ctlp_Even_c. It will then annotate each node with its parity.
A node in a formula with sharing may have both parities and a descendant
of a XOR or EQ node will have both. Only backward CTL formulae are
considered.]
SideEffects [changes the negation_parity fields of all nodes in the formula]
******************************************************************************/
void
Ctlp_FormulaNegations(
Ctlp_Formula_t * formula,
Ctlp_Parity_t parity)
{
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *leftChild;
Ctlp_Formula_t *rightChild;
Ctlp_Parity_t newparity;
assert(formula != NIL(Ctlp_Formula_t));
if (formula->negation_parity == parity)
return; /* already done */
if (formula->negation_parity != Ctlp_NoParity_c)
parity = Ctlp_EvenOdd_c; /* reconverging paths with different parity */
formula->negation_parity = parity;
formulaType = Ctlp_FormulaReadType(formula);
leftChild = Ctlp_FormulaReadLeftChild(formula);
rightChild = Ctlp_FormulaReadRightChild(formula);
switch (formulaType) {
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EF_c:
Ctlp_FormulaNegations(leftChild,parity);
break;
case Ctlp_AU_c:
case Ctlp_EU_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
Ctlp_FormulaNegations(leftChild,parity);
Ctlp_FormulaNegations(rightChild,parity);
break;
case Ctlp_NOT_c:
if (parity == Ctlp_Even_c)
newparity = Ctlp_Odd_c;
else if (parity == Ctlp_Odd_c)
newparity = Ctlp_Even_c;
else newparity = Ctlp_EvenOdd_c;
Ctlp_FormulaNegations(leftChild,newparity);
break;
case Ctlp_THEN_c:
if (parity == Ctlp_Even_c)
newparity = Ctlp_Odd_c;
else if (parity == Ctlp_Odd_c)
newparity = Ctlp_Even_c;
else newparity = Ctlp_EvenOdd_c;
Ctlp_FormulaNegations(leftChild,newparity);
Ctlp_FormulaNegations(rightChild,parity);
break;
case Ctlp_XOR_c:
case Ctlp_EQ_c:
Ctlp_FormulaNegations(leftChild,Ctlp_EvenOdd_c);
Ctlp_FormulaNegations(rightChild,Ctlp_EvenOdd_c);
break;
default:
break;
}
}
/**Function********************************************************************
Synopsis [Checks whether an ACTL formula is W-ACTL.]
Description [Test if the binary operators in an ACTL formula have at
least one propositional formula as one of the operands. If not return
Ctlp_NONWACTL_c, else return either Ctlp_WACTLsimple_c for propositional
formulae or Ctlp_WACTLstate_c for formulae containing temporal operators.
A W-ACTL formula must contain no exitential operators and no forward
operators. XOR and EQ are allowed only in propositional subformulae.]
SideEffects [none]
******************************************************************************/
Ctlp_FormulaACTLSubClass
Ctlp_CheckIfWACTL(
Ctlp_Formula_t *formula)
{
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *rightFormula, *leftFormula;
Ctlp_FormulaACTLSubClass resultLeft, resultRight;
assert(formula != NIL(Ctlp_Formula_t));
if(formula == NIL(Ctlp_Formula_t))
return Ctlp_WACTLsimple_c;
formulaType = Ctlp_FormulaReadType(formula);
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
/* Depending on the formula type, create result or recur. */
switch (formulaType) {
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
resultLeft = Ctlp_CheckIfWACTL(leftFormula);
if (resultLeft == Ctlp_NONWACTL_c)
return Ctlp_NONWACTL_c;
else
return Ctlp_WACTLstate_c;
break;
case Ctlp_AU_c:
resultLeft = Ctlp_CheckIfWACTL(leftFormula);
if (resultLeft == Ctlp_NONWACTL_c)
return Ctlp_NONWACTL_c;
resultRight = Ctlp_CheckIfWACTL(rightFormula);
if (resultRight == Ctlp_NONWACTL_c)
return Ctlp_NONWACTL_c;
if (resultLeft == Ctlp_WACTLsimple_c || resultRight == Ctlp_WACTLsimple_c)
return Ctlp_WACTLstate_c;
else
return Ctlp_NONWACTL_c;
break;
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_THEN_c:
resultLeft = Ctlp_CheckIfWACTL(leftFormula);
if (resultLeft == Ctlp_NONWACTL_c) {
return Ctlp_NONWACTL_c;
} else {
resultRight = Ctlp_CheckIfWACTL(rightFormula);
if (resultRight == Ctlp_WACTLsimple_c) {
return resultLeft;
} else if (resultLeft == Ctlp_WACTLsimple_c) {
return resultRight;
} else {
return Ctlp_NONWACTL_c;
}
}
break;
case Ctlp_NOT_c:
resultLeft = Ctlp_CheckIfWACTL(leftFormula);
return resultLeft;
break;
case Ctlp_XOR_c:
case Ctlp_EQ_c:
resultLeft = Ctlp_CheckIfWACTL(leftFormula);
if (resultLeft != Ctlp_WACTLsimple_c) {
return Ctlp_NONWACTL_c;
} else {
resultRight = Ctlp_CheckIfWACTL(rightFormula);
if (resultRight == Ctlp_WACTLsimple_c)
return Ctlp_WACTLsimple_c;
else
return Ctlp_NONWACTL_c;
}
break;
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
return Ctlp_WACTLsimple_c;
break;
default:
fprintf(vis_stderr, "#Ctlp Result : The formula should be in Universal operators!\n");
return Ctlp_NONWACTL_c;
break;
}
} /* End of Ctlp_CheckTypeOfExistentialFormula */
/**Function********************************************************************
Synopsis [Returns original formula corresponding to converted formula.]
SideEffects []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaReadOriginalFormula(
Ctlp_Formula_t * formula)
{
return formula->dbgInfo.originalFormula;
}
/**Function********************************************************************
Synopsis [Frees a formula if no other formula refers to it as a
sub-formula.]
Description [The function decrements the refCount of the formula. As a
consequence, if the refCount becomes 0, the formula is freed.]
SideEffects []
SeeAlso [CtlpFormulaFree, CtlpDecrementRefCount]
******************************************************************************/
void
Ctlp_FormulaFree(
Ctlp_Formula_t *formula)
{
CtlpFormulaDecrementRefCount(formula);
}
/**Function********************************************************************
Synopsis [Recursively frees states, underapprox and overapprox fields of
Ctlp_Formula_t, and the debug data]
Description []
SideEffects []
SeeAlso [Ctlp_FormulaFree]
******************************************************************************/
void
Ctlp_FlushStates(
Ctlp_Formula_t * formula)
{
if (formula != NIL(Ctlp_Formula_t)) {
if (formula->type != Ctlp_ID_c){
if (formula->left != NIL(Ctlp_Formula_t)) {
Ctlp_FlushStates(formula->left);
}
if (formula->right != NIL(Ctlp_Formula_t)) {
Ctlp_FlushStates(formula->right);
}
}
if (formula->states != NIL(mdd_t)){
mdd_free(formula->states);
formula->states = NIL(mdd_t);
}
if (formula->underapprox != NIL(mdd_t)){
mdd_free(formula->underapprox);
formula->underapprox = NIL(mdd_t);
}
if (formula->overapprox != NIL(mdd_t)){
mdd_free(formula->overapprox);
formula->overapprox = NIL(mdd_t);
}
if (formula->dbgInfo.data != NIL(void)){
(*formula->dbgInfo.freeFn)(formula);
formula->dbgInfo.data = NIL(void);
}
}
}
/**Function********************************************************************
Synopsis [Duplicates a CTL formula.]
Description [Recursively duplicate a formula. Does nothing if the formula
is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo, and
in general all the information that is used to annotate the formula.]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaDup(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
if ( formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
result = ALLOC(Ctlp_Formula_t, 1);
result->type = formula->type;
result->states = NIL(mdd_t);
result->underapprox = NIL(mdd_t);
result->overapprox = NIL(mdd_t);
result->latest = Ctlp_Incomparable_c;
result->Bottomstates = NIL(array_t);
result->Topstates = NIL(array_t);
result->negation_parity = Ctlp_NoParity_c;
result->leaves = formula->leaves == NIL(array_t) ?
NIL(array_t) : array_dup(formula->leaves);
result->matchfound_top = NIL(array_t);
result->matchelement_top = NIL(array_t);
result->matchfound_bot = NIL(array_t);
result->matchelement_bot = NIL(array_t);
result->refCount = 1;
result->dbgInfo.data = NIL(void);
result->dbgInfo.freeFn = (Ctlp_DbgInfoFreeFn) NULL;
result->dbgInfo.convertedFlag = FALSE;
result->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
result->top = 0;
result->compareValue = 0;
if ( formula->type != Ctlp_ID_c ) {
result->left = Ctlp_FormulaDup( formula->left );
result->right = Ctlp_FormulaDup( formula->right );
}
else {
result->left = (Ctlp_Formula_t *) util_strsav((char *)formula->left );
result->right = (Ctlp_Formula_t *) util_strsav((char *)formula->right );
}
result->share = 1;
result->BotOnionRings = NIL(array_t);
result->TopOnionRings = NIL(array_t);
return result;
}
/**Function********************************************************************
Synopsis [Complements a CTL formula.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConverttoComplement(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
result = Ctlp_FormulaCreate(Ctlp_NOT_c,formula,NIL(Ctlp_Formula_t));
CtlpFormulaIncrementRefCount(formula);
#if 0
result = FormulaCreateWithType(Ctlp_NOT_c);
result->left = FormulaCreateWithType(formula->type);
result->left->left = formula->left;
result->left->right = formula->right;
switch (formula->type) {
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
case Ctlp_Init_c:
break;
default:
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
break;
}
#endif
return result;
} /* Ctlp_FormulaConverttoComplement */
/**Function********************************************************************
Synopsis [Converts AFp to A (TRUE) U p.]
Description []
SideEffects [Should be called only for AF formula]
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertAFtoAU(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
/* AFf --> (A true U f) */
assert(formula->type == Ctlp_AF_c);
result = FormulaCreateWithType(Ctlp_AU_c);
result->left = FormulaCreateWithType(Ctlp_TRUE_c);
result->right = formula->left;
CtlpFormulaIncrementRefCount(formula->left);
return result;
}
/**Function********************************************************************
Synopsis [Converts EFp to p + EX(EFp).]
Description []
SideEffects [Should be called only for EF formula]
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertEFtoOR(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
/* EFf --> f + EX(EF(f)) */
assert(formula->type == Ctlp_EF_c);
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = formula->left;
result->right = FormulaCreateWithType(Ctlp_EX_c);
result->right->left = formula;
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula);
return result;
}
/**Function********************************************************************
Synopsis [Converts EpUq to q + p*EX(EpUq).]
Description []
SideEffects [Should be called only for EU formula]
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertEUtoOR(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
assert(formula->type == Ctlp_EU_c);
/* E(f1)U(f2) --> f2 + f1*EX( E(f1)U(f2) ) */
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = formula->right;
result->right = FormulaCreateWithType(Ctlp_AND_c);
result->right->left = formula->left;
result->right->right = FormulaCreateWithType(Ctlp_EX_c);
result->right->right->left = formula;
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
CtlpFormulaIncrementRefCount(formula);
return result;
}
/**Function********************************************************************
Synopsis [Convert p^q to !p*q + p*!q.]
Description []
SideEffects [Should be called only for XOR formula]
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertXORtoOR(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
assert(formula->type == Ctlp_XOR_c);
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = FormulaCreateWithType(Ctlp_AND_c);
result->right = FormulaCreateWithType(Ctlp_AND_c);
result->left->left = Ctlp_FormulaConverttoComplement(formula->left);
result->left->right = formula->right;
result->right->left = formula->left;
result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
return result;
}
/**Function********************************************************************
Synopsis [Converts p<->q to p*q + !p*!q.]
Description []
SideEffects [Should be called only for EQ formula]
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertEQtoOR(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
assert(formula->type == Ctlp_EQ_c);
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = FormulaCreateWithType(Ctlp_AND_c);
result->right = FormulaCreateWithType(Ctlp_AND_c);
result->left->left = formula->left;
result->left->right = formula->right;
result->right->left = Ctlp_FormulaConverttoComplement(formula->left);
result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
return result;
}
/**Function********************************************************************
Synopsis [Returns formula with a negation pushed down]
Description [Returns formula with a negation pushed down. It is assumed that
the formula being passsed to it is not a proposition]
SideEffects []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaPushNegation(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *result;
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
switch(formula->type) {
/*
* The cases are listed in rough order of their expected frequency.
*/
case Ctlp_OR_c: /*!(f1 v f2) = !f1 * !f2*/
result = FormulaCreateWithType(Ctlp_AND_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
result->right = Ctlp_FormulaConverttoComplement(formula->right);
break;
case Ctlp_AND_c: /*!(f1 * f2) = !f1 v !f2*/
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
result->right = Ctlp_FormulaConverttoComplement(formula->right);
break;
case Ctlp_THEN_c: /*!(f1 -> f2) = !(!f1 v f2) = f1 * !f2 */
result = FormulaCreateWithType(Ctlp_AND_c);
result->left = formula->left;
CtlpFormulaIncrementRefCount(formula->left);
result->right = Ctlp_FormulaConverttoComplement(formula->right);
break;
case Ctlp_XOR_c: /*!(f1 ^ f2) = f1 <-> f2*/
result = FormulaCreateWithType(Ctlp_EQ_c);
result->left = formula->left;
result->right = formula->right;
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
break;
case Ctlp_EQ_c: /*!(f1 <-> f2) = f1 ^ f2*/
result = FormulaCreateWithType(Ctlp_XOR_c);
result->left = formula->left;
result->right = formula->right;
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
break;
case Ctlp_NOT_c:/* !(!f1) = f1*/
result = formula->left;
CtlpFormulaIncrementRefCount(formula->left);
break;
case Ctlp_EX_c:/* !(EX(f1)) = AX(!f1)*/
result = FormulaCreateWithType(Ctlp_AX_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_EG_c: /*!(EG(f1)) = AF(!f1)*/
result = FormulaCreateWithType(Ctlp_AF_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_EF_c: /*!(EF(f1)) = AG(!f1)*/
result = FormulaCreateWithType(Ctlp_AG_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_EU_c: /* !(EpUq) = A(!q)U(!(p+q) + AG(!q))*/
result = FormulaCreateWithType(Ctlp_AU_c);
result->left = Ctlp_FormulaConverttoComplement(formula->right);
result->right = FormulaCreateWithType(Ctlp_OR_c);
result->right->left = FormulaCreateWithType(Ctlp_NOT_c);
result->right->left->left = FormulaCreateWithType(Ctlp_OR_c);
result->right->left->left->left = formula->left;
result->right->left->left->right = formula->right;
result->right->right = FormulaCreateWithType(Ctlp_AG_c);
result->right->right->left = Ctlp_FormulaConverttoComplement(formula->right);
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
break;
case Ctlp_AX_c:/* !AX(f1) = EX(!f1)*/
result = FormulaCreateWithType(Ctlp_EX_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_AG_c:/* !AG(f1) = EF(!f1) */
result = FormulaCreateWithType(Ctlp_EF_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_AF_c: /* !AF(f1) = EG(!f1)*/
result = FormulaCreateWithType(Ctlp_EG_c);
result->left = Ctlp_FormulaConverttoComplement(formula->left);
break;
case Ctlp_AU_c: /* !(ApUq) = (E(!q)U(!(p+q)))+(EG!q)*/
result = FormulaCreateWithType(Ctlp_OR_c);
result->left = FormulaCreateWithType(Ctlp_EU_c);
result->left->left = Ctlp_FormulaConverttoComplement(formula->right);
result->left->right = FormulaCreateWithType(Ctlp_NOT_c);
result->left->right->left= FormulaCreateWithType(Ctlp_OR_c);
result->left->right->left->left = formula->left;
result->left->right->left->right = formula->right;
result->right = FormulaCreateWithType(Ctlp_EG_c);
result->right->left = Ctlp_FormulaConverttoComplement(formula->right);
CtlpFormulaIncrementRefCount(formula->left);
CtlpFormulaIncrementRefCount(formula->right);
break;
case Ctlp_TRUE_c:/* !TRUE = FALSE*/
result = FormulaCreateWithType(Ctlp_FALSE_c);
break;
case Ctlp_FALSE_c:/*!FALSE = TRUE*/
result = FormulaCreateWithType(Ctlp_TRUE_c);
break;
case Ctlp_Init_c: /* ???*/
case Ctlp_Cmp_c: /* ???*/
/* if (formula->compareValue == 0)
tmpString = util_strcat3("[", s1, "] = ");
else
tmpString = util_strcat3("[", s1, "] != ");
result = util_strcat3(tmpString, s2, "");
break;*/
case Ctlp_FwdU_c: /* ???*/
case Ctlp_FwdG_c: /* ??? */
case Ctlp_EY_c: /* ??? */
result = formula;
break;
default:
fail("Unexpected type");
}
return result;
}
/*****************************************************************************/
/**Function********************************************************************
Synopsis [Frees an array of CTL formulas.]
Description [Calls CtlpFormulaDecrementRefCount on each formula in
formulaArray, and then frees the array itself. It is okay to call this
function with an empty array, but it is an error to call it with a NULL
array.]
SideEffects []
SeeAlso [Ctlp_FormulaFree]
******************************************************************************/
void
Ctlp_FormulaArrayFree(
array_t * formulaArray /* of Ctlp_Formula_t */)
{
int i;
int numFormulas = array_n(formulaArray);
assert(formulaArray != NIL(array_t));
for (i = 0; i < numFormulas; i++) {
Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
CtlpFormulaDecrementRefCount(formula);
}
array_free(formulaArray);
}
/**Function********************************************************************
Synopsis [Converts a CTL formula to existential form.]
Description [Converts a CTL formula to existential form. That is, all
universal path quantifiers are replaced with the appropriate combination of
existential quantifiers and Boolean negation. Also converts "finally"
operators to "until" operators.
Returns a new formula that shares absolutely nothing with the original
formula (not even the strings). Also, the new formula does not have any MDDs
associated with it. The "originalFormula" field of each new subformula is
set to point to the formula passed as an argument. In addition, if (and only
if) the original formula is of type AG, AX, AU, AF, or EF, the "converted
flag" is set. Returns NULL if called with a NULL formula.
Note: the debugger takes advantage of the exact way that the conversion is
done. Hence, you cannot play around much with the syntax of the converted
formula.
A list of conversion rules shouls be included here (RB).
AG phi turns into !EU(true,! phi'), where the top ! has converted set
and points to the AG, and phi' points to phi.
AU?
AX?
Any others?
]
SideEffects []
SeeAlso [Ctlp_FormulaArrayConvertToExistentialForm,
Ctlp_ConvertToSimpleExistentialForm]
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertToExistentialForm(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *new_;
char *variableNameCopy, *valueNameCopy;
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
/*
* Recursively convert each subformula.
*/
switch(formula->type) {
case Ctlp_EF_c:
/* EFf --> (E true U f) */
new_ = FormulaCreateWithType(Ctlp_EU_c);
new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->right = Ctlp_FormulaConvertToExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AX_c:
/* AXf --> !(EX(!f)) */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EX_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AG_c:
/* AGf --> ![(E true U !f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EU_c);
new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->right->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AF_c:
/* AFf --> ![EG(!f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EG_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AU_c:
/* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
new_->left->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left); /* f */
new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->left->right->right->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_ID_c:
/* Make a copy of the name, and create a new formula. */
variableNameCopy = util_strsav((char *)(formula->left));
valueNameCopy = util_strsav((char *)(formula->right));
new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
break;
case Ctlp_THEN_c:
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EU_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_XOR_c:
case Ctlp_EQ_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
/* These are already in the correct form. Just convert subformulas. */
new_ = FormulaCreateWithType(formula->type);
new_->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
new_->right = Ctlp_FormulaConvertToExistentialForm(formula->right);
break;
default:
fail("Unexpected type");
}
new_->dbgInfo.originalFormula = formula;
return new_;
}
/**Function********************************************************************
Synopsis [Converts a CTL formula to simple existential form.]
Description [Converts a CTL formula to simple existential form.
That is, all universal path quantifiers are replaced with the
appropriate combination of existential quantifiers and Boolean
negation. Only `NOT' and `AND' Boolean operators are allowed. Also
converts "finally" operators to "until" operators.
The converted bit is set in the converted formula only when temporal
operators are converted, not when boolean operators are converted.
A new formula is created that needs to be freed seperately.]
SideEffects []
Remarks [Ctl formulas in simple existential form are incompatible
with the mc debug routines. The reason is that the debug routines
count on a very specific form of the converted formula to conclude
what the original formula was.]
SeeAlso [Ctlp_FormulaArrayConvertToExistentialForm]
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaConvertToSimpleExistentialForm(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *new_;
char *variableNameCopy, *valueNameCopy;
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
/*
* Recursively convert each subformula.
*/
switch(formula->type) {
case Ctlp_EF_c:
/* EFf --> (E true U f) */
new_ = FormulaCreateWithType(Ctlp_EU_c);
new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AX_c:
/* AXf --> !(EX(!f)) */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EX_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AG_c:
/* AGf --> ![(E true U !f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EU_c);
new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AF_c:
/* AFf --> ![EG(!f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EG_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AU_c:
/* A[fUg] --> !(E[!g U (!f*!g)]) * !(EG!g)) */
new_ = FormulaCreateWithType(Ctlp_AND_c); /* top */
new_->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
new_->right->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->right->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
new_->right->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
new_->right->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
new_->right->left->right->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left); /* f */
new_->right->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->right->left->right->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_ID_c:
/* Make a copy of the name, and create a new formula. */
variableNameCopy = util_strsav((char *)(formula->left));
valueNameCopy = util_strsav((char *)(formula->right));
new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
break;
/* RB: I think THEN (and also OR, and maybe some others) should also have converted set. */
case Ctlp_THEN_c:
/* p->q --> !(p * !q) */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_AND_c);
new_->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
break;
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EU_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
/* These are already in the correct form. Just convert subformulas. */
new_ = FormulaCreateWithType(formula->type);
new_->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
break;
case Ctlp_OR_c:
/* p + q --> !(!p * !q) */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_AND_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->left->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
break;
case Ctlp_XOR_c:
/* p ^ q --> !(p * q) * !(!p * !q) */
new_ = FormulaCreateWithType(Ctlp_AND_c);
new_->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
new_->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->left->left->right =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
new_->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->right->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->right->left->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
break;
case Ctlp_EQ_c:
/* p <-> q --> !(p * !q) * !(!p * q) */
new_ = FormulaCreateWithType(Ctlp_AND_c);
new_->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
new_->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->right->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
new_->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->right->left->left->left =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
new_->right->left->right =
Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
break;
default:
fail("Unexpected type");
}
new_->dbgInfo.originalFormula = formula;
return new_;
}
/**Function********************************************************************
Synopsis [Converts an array of CTL formulas to existential form.]
Description [Calls Ctlp_FormulaConvertToExistentialForm on each formula. It
is okay to call this function with an empty array (in which case an empty
array is returned), but it is an error to call it with a NULL array.
All formulas in the array are copied, and hence Ctlp_FormulaArrayFree() needs
to be called on the result at the end.]
SideEffects []
SeeAlso [Ctlp_FormulaConvertToExistentialForm]
******************************************************************************/
array_t *
Ctlp_FormulaArrayConvertToExistentialFormTree(
array_t * formulaArray /* of Ctlp_Formula_t */)
{
int i;
int numFormulas = array_n(formulaArray);
array_t *convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
assert(formulaArray != NIL(array_t));
for (i = 0; i < numFormulas; i++) {
Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
Ctlp_Formula_t *convertedFormula = Ctlp_FormulaConvertToExistentialForm(formula);
array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
}
return convertedArray;
}
/**Function********************************************************************
Synopsis [Converts an array of CTL formulas to simple existential form.]
Description [Calls Ctlp_FormulaConvertToSimpleExistentialForm on
each formula. It is okay to call this function with an empty array
(in which case an empty array is returned), but it is an error to
call it with a NULL array.]
SideEffects []
SeeAlso [Ctlp_FormulaConvertToExistentialForm]
******************************************************************************/
array_t *
Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
array_t * formulaArray /* of Ctlp_Formula_t */)
{
int i;
int numFormulas;
array_t *convertedArray;
assert( formulaArray != NIL(array_t));
numFormulas = array_n(formulaArray);
convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
for (i = 0; i < numFormulas; i++) {
Ctlp_Formula_t *formula;
Ctlp_Formula_t *convertedFormula;
formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
convertedFormula = Ctlp_FormulaConvertToSimpleExistentialForm(formula);
array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
}
return convertedArray;
}
/**Function********************************************************************
Synopsis [Converts an array of CTL formulae to a multi-rooted DAG.]
Description [The function hashes each subformula of a formula
(including the formula itself) into a uniqueTable. It returns an
array containing the roots of the multi-rooted DAG thus created by
the sharing of the subformulae. It is okay to call this function
with an empty array (in which case an empty array is returned), but
it is an error to call it with a NULL array.]
SideEffects [A formula in formulaArray might be freed if it had been
encountered as a subformula of some other formula. Other formulae in
formulaArray might be present in the returned array. Therefore, the
formulae in formulaArray should not be freed. Only formulaArray
itself should be freed.
RB: What does that mean?
I understand this as follows. Copies of the formulae are not made,
but rather pointers to the argument subformulae are kept. Hence, not only
should the formulae in the result not be freed, but also you cannot free the
argument before you are done with the result. Furthermore, by invocation of
this function, the argument gets altered. It is still valid, but pointers
may have changed. Is this correct?
RB rewrite: A formula in formulaArray is freed if it is encountered as a
subformula of some other formula. Other formulae in formulaArray might be
present in the returned array. Therefore, the formulae in formulaArray should
not be freed. Only formulaArray itself should be freed.]
SeeAlso []
******************************************************************************/
array_t *
Ctlp_FormulaArrayConvertToDAG(
array_t *formulaArray)
{
int i;
Ctlp_Formula_t *formula, *uniqueFormula;
st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash);
int numFormulae = array_n(formulaArray);
array_t *rootsOfFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
assert(formulaArray != NIL(array_t));
for(i=0; i < numFormulae; i++) {
formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable);
if(uniqueFormula != formula) {
CtlpFormulaDecrementRefCount(formula);
CtlpFormulaIncrementRefCount(uniqueFormula);
array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula);
}
else
array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, formula);
}
st_free_table(uniqueTable);
return rootsOfFormulaDAG;
}
/**Function********************************************************************
Synopsis [Converts a DAG of CTL formulae to a DAG of existential CTL
formulae.]
Description [The function converts a DAG of CTL formulae to a DAG of
existential CTL formulae. The function recursively converts each
subformula of each of the formulae in the DAG and remembers the
converted formula in the field states. It is okay to call this
function with an empty array (in which case an empty array is
returned), but it is an error to call it with a NULL array.
The states fileds in the formula need to be NULL.]
SideEffects []
SeeAlso [FormulaConvertToExistentialDAG]
******************************************************************************/
array_t *
Ctlp_FormulaDAGConvertToExistentialFormDAG(
array_t *formulaDAG)
{
int i;
Ctlp_Formula_t *formula;
int numFormulae = array_n(formulaDAG);
array_t *existentialFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
assert( formulaDAG != NIL(array_t));
for(i=0; itype = type;
formula->left = (Ctlp_Formula_t *)left;
formula->right = (Ctlp_Formula_t *)right;
formula->refCount = 1;
formula->states = NIL(mdd_t);
formula->underapprox = NIL(mdd_t);
formula->overapprox = NIL(mdd_t);
formula->Topstates = NIL(array_t);
formula->Bottomstates = NIL(array_t);
formula->leaves = NIL(array_t);
formula->matchfound_top = NIL(array_t);
formula->matchelement_top = NIL(array_t);
formula->matchfound_bot = NIL(array_t);
formula->matchelement_bot = NIL(array_t);
formula->negation_parity = Ctlp_NoParity_c;
formula->share = 1;
formula->dbgInfo.data = NIL(void);
formula->dbgInfo.freeFn = (Ctlp_DbgInfoFreeFn) NULL;
formula->dbgInfo.convertedFlag = FALSE;
formula->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
formula->top = 0;
formula->compareValue = 0;
formula->latest = Ctlp_Incomparable_c;
formula->BotOnionRings = NIL(array_t);
formula->TopOnionRings = NIL(array_t);
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula with disjunction of atomic propositions]
Description [This function returns Ctlp_Formula_t for name = {v1,v2,...}.
In case of failure, a NULL pointer is returned.]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateOr(
char *name,
char *valueStr)
{
Ctlp_Formula_t *formula, *tempFormula;
char *preStr;
preStr = strtok(valueStr,",");
formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
util_strsav(preStr));
if (formula == NIL(Ctlp_Formula_t)) {
return NIL(Ctlp_Formula_t);
}
while ((preStr = strtok(NIL(char),",")) != NIL(char)) {
tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
util_strsav(preStr));
if (tempFormula == NIL(Ctlp_Formula_t)) {
Ctlp_FormulaFree(formula);
return NIL(Ctlp_Formula_t);
}
formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
}
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula with conjunction of atomic propositions]
Description [This function returns Ctlp_Formula_t for nameVector = value,
nameVector is a form of var[i:j] or var and value is any integer n or
binary string starting with 'b', for instance, b0011. If n is not
fitted in var[i:j] or size of binary string is not matched with
var[i:j], NULL pointer is returned]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateVectorAnd(
char *nameVector,
char *value)
{
Ctlp_Formula_t *formula, *tempFormula;
int startValue, endValue, inc, i,j, interval,startInd;
char *binValueStr, *varName, *name;
char *bitValue;
varName = CtlpGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc);
binValueStr = ALLOC(char,interval+1);
if (!CtlpStringChangeValueStrToBinString(value,binValueStr,interval) ){
FREE(varName);
FREE(binValueStr);
return NIL(Ctlp_Formula_t);
}
name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
(void) sprintf(name,"%s[%d]",varName,startValue);
(void) CtlpChangeBracket(name);
bitValue = ALLOC(char,2);
bitValue[0] = binValueStr[0];
bitValue[1] = '\0';
formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
util_strsav(bitValue));
j = 0;
startInd = startValue;
for(i=startValue;i!=endValue;i=i+inc){
startInd += inc;
j++;
(void) sprintf(name,"%s[%d]",varName,startInd);
(void) CtlpChangeBracket(name);
bitValue[0] = binValueStr[j];
tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
util_strsav(bitValue));
formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
}
FREE(varName);
FREE(name);
FREE(binValueStr);
FREE(bitValue);
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula with OR of Vector AND]
Description [This function returns Ctlp_Formula_t for nameVector = valueStr,
nameVector is a form of var[i:j] or var, valueStr is "k,l,...,q",
and k,l,...,q is either integer or binary string. Binary string starting
with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of
binary string is not matched with var[i:j], NULL pointer is returned]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateVectorOr(
char *nameVector,
char *valueStr)
{
Ctlp_Formula_t *formula,*tempFormula;
char *preStr;
preStr = strtok(valueStr,",");
formula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
if ( formula == NIL(Ctlp_Formula_t)){
return NIL(Ctlp_Formula_t);
}
while( (preStr = strtok(NIL(char),",")) != NIL(char) ){
tempFormula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
if ( tempFormula == NIL(Ctlp_Formula_t)){
Ctlp_FormulaFree(formula);
return NIL(Ctlp_Formula_t);
}
formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
}
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula for equivalent property]
Description [This function assumes that each child is defined in binary
domain. Enumerate type is not supported]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateEquiv(
char *left,
char *right)
{
Ctlp_Formula_t *formula,*formula1,*formula2;
char *one;
char *zero;
one = "1";
zero = "0";
formula1 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(left),
util_strsav(one));
formula2 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(right),
util_strsav(zero));
formula = Ctlp_FormulaCreate(Ctlp_XOR_c,formula1,formula2);
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula for equivalent of vector]
Description [This function returns a formula, which is the AND of a bitwise
equivalence]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateVectorEquiv(
char *left,
char *right)
{
Ctlp_Formula_t *formula,*tempFormula;
char *leftName,*rightName;
char *leftVar, *rightVar;
int leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval;
int leftInc,rightInc,leftInd,rightInd,i;
leftName = CtlpGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc);
rightName = CtlpGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc);
if (leftInterval != rightInterval){
return NIL(Ctlp_Formula_t);
}
leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
(void) sprintf(leftVar,"%s[%d]",leftName,leftStart);
(void) CtlpChangeBracket(leftVar);
rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
(void) sprintf(rightVar,"%s[%d]",rightName,rightStart);
(void) CtlpChangeBracket(rightVar);
formula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
leftInd = leftStart;
rightInd = rightStart;
for(i=leftStart;i!=leftEnd;i+=leftInc){
leftInd += leftInc;
rightInd += rightInc;
(void) sprintf(leftVar,"%s[%d]",leftName,leftInd);
(void) CtlpChangeBracket(leftVar);
(void) sprintf(rightVar,"%s[%d]",rightName,rightInd);
(void) CtlpChangeBracket(rightVar);
tempFormula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
}
FREE(leftName);
FREE(rightName);
FREE(leftVar);
FREE(rightVar);
return formula;
}
/**Function********************************************************************
Synopsis [Creates a CTL formula for multiple AX]
Description [This function returns a formula, which is the multiple
times of AX. The given string includes the number of depth]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateAXMult(
char *string,
Ctlp_Formula_t *formula)
{
int i,num;
char *str, *ptr;
Ctlp_Formula_t *result;
str = strchr(string,':');
if ( str == NULL) return(NIL(Ctlp_Formula_t));
str++;
num = strtol(str,&ptr,0);
if (num<=0){
return (NIL(Ctlp_Formula_t));
}
result = Ctlp_FormulaCreate(Ctlp_AX_c,formula,NIL(Ctlp_Formula_t));
for(i=1;ileft = FormulaCreateWithType(Ctlp_Init_c);
if (compareValue == 0) {
forwardFormula->right = FormulaCreateWithType(Ctlp_NOT_c);
forwardFormula->right->left = existentialFormula;
} else
forwardFormula->right = existentialFormula;
forwardFormula->right->states = (mdd_t *)forwardFormula;
/* if formula was converted before, keep that reference */
if(existentialFormula->dbgInfo.originalFormula != NIL(Ctlp_Formula_t))
forwardFormula->dbgInfo.originalFormula =
existentialFormula->dbgInfo.originalFormula;
else
forwardFormula->dbgInfo.originalFormula = existentialFormula;
forwardFormula->top = 1;
forwardFormula->compareValue = compareValue;
FormulaConvertToForward(forwardFormula->right, compareValue);
CtlpFormulaSetStatesToNULL(forwardFormula);
FormulaInsertForwardCompareNodes(forwardFormula, NULL, compareValue);
array_insert(Ctlp_Formula_t *, forwardFormulaArray, i, forwardFormula);
}
if (doNotShareFlag)
return(forwardFormulaArray);
forwardDagArray = Ctlp_FormulaArrayConvertToDAG(forwardFormulaArray);
array_free(forwardFormulaArray);
return forwardDagArray;
}
/**Function********************************************************************
Synopsis [Returns a string for each formula type.]
Description [Returns a string for each formula type.]
SideEffects []
SeeAlso []
******************************************************************************/
char *
Ctlp_FormulaGetTypeString(Ctlp_Formula_t *formula)
{
char *result;
switch(formula->type) {
/*
* The cases are listed in rough order of their expected frequency.
*/
case Ctlp_ID_c:
result = util_strsav("ID");
break;
case Ctlp_OR_c:
result = util_strsav("OR");
break;
case Ctlp_AND_c:
result = util_strsav("AND");
break;
case Ctlp_THEN_c:
result = util_strsav("THEN");
break;
case Ctlp_XOR_c:
result = util_strsav("XOR");
break;
case Ctlp_EQ_c:
result = util_strsav("EQ");
break;
case Ctlp_NOT_c:
result = util_strsav("NOT");
break;
case Ctlp_EX_c:
result = util_strsav("EX");
break;
case Ctlp_EG_c:
result = util_strsav("EG");
break;
case Ctlp_EF_c:
result = util_strsav("EF");
break;
case Ctlp_EU_c:
result = util_strsav("EU");
break;
case Ctlp_AX_c:
result = util_strsav("AX");
break;
case Ctlp_AG_c:
result = util_strsav("AG");
break;
case Ctlp_AF_c:
result = util_strsav("AF");
break;
case Ctlp_AU_c:
result = util_strsav("AU");
break;
case Ctlp_TRUE_c:
result = util_strsav("TRUE");
break;
case Ctlp_FALSE_c:
result = util_strsav("FALSE");
break;
case Ctlp_Init_c:
result = util_strsav("Init");
break;
case Ctlp_Cmp_c:
result = util_strsav("Cmp");
break;
case Ctlp_FwdU_c:
result = util_strsav("FwdU");
break;
case Ctlp_FwdG_c:
result = util_strsav("FwdG");
break;
case Ctlp_EY_c:
result = util_strsav("EY");
break;
case Ctlp_EH_c:
result = util_strsav("EH");
break;
default:
fail("Unexpected type");
}
return(result);
}
/**Function********************************************************************
Synopsis [Tests if a formula is quantifier-free, ACTL, ECTL or
mixed.]
Description [Tests if a formula is Quantifier free, ACTL, ECTL or mixed. We
assume that the formula is in existential normal form, and hence only
contains existential temporal operators.
The formula is ECTL if every temporal operator appears under an even
number of negations, and it is ACTL if every temporal operator appears under
an odd number of negations. It is quantifier-free if it is both ECTL and
ACTL (i.e., no temporal operators occur), and it is mixed if it is neither
ECTL nor ACTL.]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_FormulaClass
Ctlp_CheckClassOfExistentialFormula(
Ctlp_Formula_t *formula)
{
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *rightFormula, *leftFormula;
Ctlp_FormulaClass resultLeft, resultRight, tempResult, currentClass;
assert(formula != NIL(Ctlp_Formula_t));
if(formula == NIL(Ctlp_Formula_t))
return Ctlp_QuantifierFree_c;
formulaType = Ctlp_FormulaReadType(formula);
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
/* Depending on the formula type, create result or recur */
switch (formulaType) {
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EF_c:
case Ctlp_EU_c:
case Ctlp_FwdU_c:
case Ctlp_FwdG_c:
case Ctlp_EY_c:
case Ctlp_EH_c:
resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
if (formulaType == Ctlp_EU_c || formulaType == Ctlp_FwdU_c ||
formulaType == Ctlp_FwdG_c )
resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
else
resultRight = Ctlp_QuantifierFree_c;
tempResult = CtlpResolveClass(resultLeft, resultRight);
currentClass = Ctlp_ECTL_c;
return CtlpResolveClass(currentClass, tempResult);
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_AU_c:
/* The formula is supposed to be only existential */
fprintf(vis_stdout,
"** Ctlp Error: unexpected (universal) operator type\n");
assert(0);
return Ctlp_Mixed_c;
case Ctlp_OR_c:
case Ctlp_AND_c:
resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
return CtlpResolveClass(resultLeft, resultRight);
case Ctlp_NOT_c:
tempResult = Ctlp_CheckClassOfExistentialFormula(leftFormula);
return CtlpNegateFormulaClass(tempResult);
case Ctlp_THEN_c:
resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
tempResult = CtlpNegateFormulaClass(resultLeft);
return CtlpResolveClass(tempResult, resultRight);
case Ctlp_XOR_c:
case Ctlp_EQ_c:
resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
tempResult = CtlpResolveClass(resultLeft, resultRight);
if( tempResult == Ctlp_QuantifierFree_c)
return Ctlp_QuantifierFree_c;
else
return Ctlp_Mixed_c;
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
case Ctlp_Init_c:
return Ctlp_QuantifierFree_c;
case Ctlp_Cmp_c:
return Ctlp_Mixed_c;
default:
fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
assert(0);
return Ctlp_Mixed_c;
}
} /* End of Ctlp_CheckTypeOfExistentialFormula */
/**Function********************************************************************
Synopsis [Tests if an array of simple existential formulae has only
ACTL, only ECTL or mixture of formula.]
Description [Returns Ctlp_ECTL_c if the array contains only
ECTL formulae, Ctlp_ACTL_c if it contains only ACTL formulae,
Ctlp_QuantifierFree_c if there are no quantifiers in any formulae,
and Ctlp_Mixed otherwise.]
SideEffects []
SeeAlso [Ctlp_CheckClassOfExistentialFormula]
******************************************************************************/
Ctlp_FormulaClass
Ctlp_CheckClassOfExistentialFormulaArray(
array_t *formulaArray)
{
Ctlp_FormulaClass result;
Ctlp_Formula_t *formula;
int formulanr;
result = Ctlp_QuantifierFree_c;
arrayForEachItem(Ctlp_Formula_t *, formulaArray, formulanr, formula){
Ctlp_FormulaClass formulaType;
formulaType = Ctlp_CheckClassOfExistentialFormula(formula);
result = CtlpResolveClass(result, formulaType);
if(result == Ctlp_Mixed_c)
return result;
}
return result;
} /* End of Ctlp_CheckTypeOfExistentialFormulaArray */
/**Function********************************************************************
Synopsis [Compare two formulas for equality]
Description [Checks if two formulas are syntactically the same. Equivalent
constructions such as TRUE and TRUE+FALSE are not recognized, but copies are
handled correctly, and strings are compared using strcmp.]
SideEffects []
SeeAlso [FormulaCompare]
******************************************************************************/
boolean
Ctlp_FormulaIdentical(
Ctlp_Formula_t *formula1,
Ctlp_Formula_t *formula2)
{
return(FormulaCompare((char *)formula1, (char *)formula2) == 0);
}
/**Function********************************************************************
Synopsis [Replaces non-monotonic operators in a formula.]
Description [This function takes a parse tree for a CTL formula and
transforms it into another tree that has only monotonic operators.
The non-monotonic operators are XOR and EQ.
They are replaced by eqivalent trees. Specificallt, XOR(a,b)
is replaced by OR(AND(a,NOT(b)),AND(NOT(a),b)) and
f <-> g is replaced by AND(f->g,g->f).
It is important that the original formula be a tree. The idea is that this
function should be called right after reading the formulae from file. Since
the information attached to the parse tree by the model checking procedures
is not preserved, it is also important that no such information exists.
These conditions are checked by an assertion.
This function does not deal with the forward CTL operators. Reduction to
monotonic operators should be performed before conversion to forward CTL.]
SideEffects [The argument is modified. The new formulae will apprear
when they are printed out.]
SeeAlso [Ctlp_FormulaArrayMakeMonotonic]
******************************************************************************/
void
Ctlp_FormulaMakeMonotonic(
Ctlp_Formula_t *formula)
{
Ctlp_Formula_t *left, *right;
Ctlp_FormulaType type;
if (formula == NIL(Ctlp_Formula_t)) {
return;
}
/* Make sure (recursively) that this (sub)-formula is still in its pristine
* state. Specifically, that the parse graph is a tree.
*/
assert(formula->refCount == 1 &&
formula->states == NIL(mdd_t) &&
formula->underapprox == NIL(mdd_t) &&
formula->overapprox == NIL(mdd_t) &&
formula->latest == Ctlp_Incomparable_c &&
formula->dbgInfo.data == NIL(void) &&
formula->dbgInfo.freeFn == (Ctlp_DbgInfoFreeFn) NULL &&
formula->dbgInfo.convertedFlag == FALSE &&
formula->dbgInfo.originalFormula == NIL(Ctlp_Formula_t) &&
formula->top == 0 &&
formula->compareValue == 0
);
type = Ctlp_FormulaReadType(formula);
/* Leaves remain unchanged. */
if (type == Ctlp_ID_c || type == Ctlp_TRUE_c || type == Ctlp_FALSE_c) {
return;
}
/* First recursively fix the children. */
left = Ctlp_FormulaReadLeftChild(formula);
Ctlp_FormulaMakeMonotonic(left);
right = Ctlp_FormulaReadRightChild(formula);
Ctlp_FormulaMakeMonotonic(right);
/* Fix this node if it is not monotonic. */
switch (type) {
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EF_c:
case Ctlp_EU_c:
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_AU_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_THEN_c:
case Ctlp_EY_c:
case Ctlp_EH_c:
/* Nothing to be done */
break;
case Ctlp_EQ_c: {
Ctlp_Formula_t *dupLeft, *dupRight;
Ctlp_Formula_t *thenLeft, *thenRight;
dupLeft = Ctlp_FormulaDup(left);
dupRight = Ctlp_FormulaDup(right);
thenLeft = Ctlp_FormulaCreate(Ctlp_THEN_c, left, right);
thenRight = Ctlp_FormulaCreate(Ctlp_THEN_c, dupRight, dupLeft);
/* Fix the node in place. */
formula->type = Ctlp_AND_c;
formula->left = thenLeft;
formula->right = thenRight;
break;
}
case Ctlp_XOR_c: {
Ctlp_Formula_t *dupLeft, *dupRight;
Ctlp_Formula_t *negLeft, *negRight;
Ctlp_Formula_t *andLeft, *andRight;
dupLeft = Ctlp_FormulaDup(left);
dupRight = Ctlp_FormulaDup(right);
negLeft = Ctlp_FormulaCreate(Ctlp_NOT_c, dupLeft, NIL(Ctlp_Formula_t));
negRight = Ctlp_FormulaCreate(Ctlp_NOT_c, dupRight, NIL(Ctlp_Formula_t));
andLeft = Ctlp_FormulaCreate(Ctlp_AND_c, left, negRight);
andRight = Ctlp_FormulaCreate(Ctlp_AND_c, negLeft, right);
/* Fix the node in place. */
formula->type = Ctlp_OR_c;
formula->left = andLeft;
formula->right = andRight;
break;
}
default:
/* Forward CTL operators (that are not supported) and leaves (that are
* dealt with above) would fall here.
*/
fail("unexpected CTL formula type\n");
}
return;
} /* Ctlp_FormulaMakeMonotonic */
/**Function********************************************************************
Synopsis [Replaces non-monotonic operators in an array of formulae.]
Description [Apply Ctlp_FormulaMakeMonotonic to each formula in the array.]
SideEffects [The formulae in the array are modified.]
SeeAlso [Ctlp_FormulaMakeMonotonic]
******************************************************************************/
void
Ctlp_FormulaArrayMakeMonotonic(
array_t *formulaArray /* of Ctlp_Formula_t */)
{
int i;
Ctlp_Formula_t *formula;
if (formulaArray == NIL(array_t)) return;
arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formula) {
Ctlp_FormulaMakeMonotonic(formula);
}
} /* Ctlp_FormulaArrayMakeMonotonic */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Increments the reference count of a formula.]
Description [The function increments the reference count of a formula. If
the formula is NULL, the function does nothing.]
SideEffects []
SeeAlso []
******************************************************************************/
void
CtlpFormulaIncrementRefCount(
Ctlp_Formula_t *formula)
{
if(formula!=NIL(Ctlp_Formula_t)) {
++(formula->refCount);
}
}
/**Function********************************************************************
Synopsis [Decrements the reference count of a formula.]
Description [The function decrements the reference count of formula and if
the reference count reaches 0, the formula is freed. If the formula is NULL,
the function does nothing. It is an error to decrement the reference count
below 0.]
SideEffects []
SeeAlso []
******************************************************************************/
void
CtlpFormulaDecrementRefCount(
Ctlp_Formula_t *formula)
{
if(formula!=NIL(Ctlp_Formula_t)) {
assert(formula->refCount>0);
if(--(formula->refCount) == 0)
CtlpFormulaFree(formula);
}
}
/**Function********************************************************************
Synopsis [Adds formula to the end of globalFormulaArray.]
SideEffects [Manipulates the global variable globalFormulaArray.]
SeeAlso [CtlpYyparse]
******************************************************************************/
void
CtlpFormulaAddToGlobalArray(
Ctlp_Formula_t * formula)
{
array_insert_last(Ctlp_Formula_t *, globalFormulaArray, formula);
}
/**Function********************************************************************
Synopsis [Frees a CTL formula.]
Description [The function frees all memory associated with the formula,
including all MDDs and all character strings (however, does not free
dbgInfo.originalFormula). It also decrements the reference counts of its two
chidren. The function does nothing if formula is NULL.]
SideEffects []
SeeAlso [Ctlp_FormulaArrayFree]
******************************************************************************/
void
CtlpFormulaFree(
Ctlp_Formula_t * formula)
{
if (formula != NIL(Ctlp_Formula_t)) {
/*
* Free any fields that are not NULL.
*/
if (formula->type == Ctlp_ID_c) {
FREE(formula->left);
FREE(formula->right);
}
else {
if (formula->left != NIL(Ctlp_Formula_t)) {
CtlpFormulaDecrementRefCount(formula->left);
}
if (formula->right != NIL(Ctlp_Formula_t)) {
CtlpFormulaDecrementRefCount(formula->right);
}
}
if (formula->states != NIL(mdd_t))
mdd_free(formula->states);
if (formula->underapprox != NIL(mdd_t))
mdd_free(formula->underapprox);
if (formula->overapprox != NIL(mdd_t))
mdd_free(formula->overapprox);
if (formula->Bottomstates != NIL(array_t))
mdd_array_free(formula->Bottomstates);
if (formula->Topstates != NIL(array_t))
mdd_array_free(formula->Topstates);
if (formula->matchfound_top != NIL(array_t))
array_free(formula->matchfound_top);
if (formula->matchelement_top != NIL(array_t))
array_free(formula->matchelement_top);
if (formula->matchfound_bot != NIL(array_t))
array_free(formula->matchfound_bot);
if (formula->matchelement_bot != NIL(array_t))
array_free(formula->matchelement_bot);
if (formula->leaves != NIL(array_t))
array_free(formula->leaves);
if (formula->dbgInfo.data != NIL(void)) {
(*formula->dbgInfo.freeFn)(formula);
}
FREE(formula);
}
}
/**Function********************************************************************
Synopsis [Create a binary string of given value with size of interval ]
Description [The value is a binary string starting with 'b',
a hexadecimal string starting with 'x', or an
integer string. If Value is not fitted in the interval, 0 is return.
Otherwise 1 is returned. Result string is saved at given pointer.]
SideEffects []
SeeAlso []
******************************************************************************/
int
CtlpStringChangeValueStrToBinString(
char *value,
char *binValueStr,
int interval)
{
int i;
long int num, mask;
double maxNum;
char *ptr;
mask = 1;
maxNum = pow(2.0,(double)interval);
errno = 0;
if(value[0] == 'b'){
if ((int)strlen(value)-1 == interval){
for(i=1;i<=interval;i++){
if (value[i] == '0' || value[i] == '1'){
binValueStr[i-1] = value[i];
}else{
return 0;
}
}
binValueStr[interval] = '\0';
}else{
return 0;
}
}else if (value[0] == 'x'){
for(i=1; i < (int)strlen(value); i++){
if (!isxdigit((int)value[i])){
return 0;
}
}
num = strtol(++value,&ptr,16);
if (errno) return 0;
if ( num >= maxNum) return 0;
for(i=0;i= maxNum) return 0;
mask = 1;
for(i=0;i]
Description []
SideEffects [The input string contains ...[num] and this function changes it
to ....]
SeeAlso []
******************************************************************************/
void
CtlpChangeBracket(
char *inStr)
{
int i, j;
char *str;
j = 0;
for (i=0;i<(int)strlen(inStr)+1;i++){
if (inStr[i] != ' '){
inStr[i-j] = inStr[i];
}else{
j++;
}
}
if (changeBracket == 0)
return;
str = strchr(inStr,'[');
if (str == NULL) return;
*str = '<';
str = strchr(inStr,']');
*str = '>';
}
/**Function********************************************************************
Synopsis [Parse a given vector string.]
Description [Parse given vector string of the form of var and
string var is returned. Other information such as i, j, interval between
i and j, and increment or decrement from i to j are saved.]
SideEffects []
SeeAlso []
******************************************************************************/
char *
CtlpGetVectorInfoFromStr(
char *str,
int *start,
int *end,
int *interval,
int *inc)
{
char *str1, *str2, *str3;
char *startStr, *endStr;
char *name, *ptr;
str1 = strchr(str,'[');
str2 = strchr(str,':');
str3 = strchr(str,']');
startStr = ALLOC(char, str2-str1);
endStr = ALLOC(char, str3-str2);
name = ALLOC(char, str1-str+1);
(void) strncpy(name, str, str1-str);
(void) strncpy(startStr, str1+1, str2-str1-1);
(void) strncpy(endStr, str2+1, str3-str2-1);
startStr[str2-str1-1] = '\0';
endStr[str3-str2-1] = '\0';
name[str1-str] = '\0';
*start = strtol(startStr,&ptr,0);
*end = strtol(endStr,&ptr,0);
if(*start > *end){
*inc = -1;
*interval = *start - *end + 1;
} else {
*inc = 1;
*interval = *end - *start + 1;
}
FREE(startStr);
FREE(endStr);
return name;
}
/**Function********************************************************************
Synopsis [Insert macro formula into symbol table.]
Description [If the name is already in table return 0, otherwise insert the
formula into the table and return 1]
SideEffects []
SeeAlso []
******************************************************************************/
int
CtlpFormulaAddToTable(
char *name,
Ctlp_Formula_t *formula,
st_table *macroTable)
{
if(macroTable == NIL(st_table)){
macroTable = st_init_table(strcmp, st_strhash);
}
if(st_is_member(macroTable, name)){
return 0;
}
st_insert(macroTable, name, (char *)formula);
return 1;
}
/**Function********************************************************************
Synopsis [Get macro formula from symbol table]
Description [If macro string is not found in table, NULL pointer is returned]
SideEffects []
SeeAlso []
******************************************************************************/
Ctlp_Formula_t *
CtlpFormulaFindInTable(
char *name,
st_table *macroTable)
{
Ctlp_Formula_t *formula;
if (st_lookup(macroTable, name, &formula)){
return (Ctlp_FormulaDup(formula));
}else{
return NIL(Ctlp_Formula_t);
}
}
/**Function********************************************************************
Synopsis [Returns the greatest lower bound of two classes]
Description [Returns the class of a formula that is the combination of a
formula of class1 and class2. Does this by computing the glb, where mixed <
ECTL < quantifierFree, and mixed < ACTL < quantifierfree.]
SideEffects []
SeeAlso [Ctlp_CheckClassOfExistentialFormula]
******************************************************************************/
Ctlp_FormulaClass
CtlpResolveClass(
Ctlp_FormulaClass class1,
Ctlp_FormulaClass class2)
{
if ((class1 == Ctlp_Mixed_c) || (class2 == Ctlp_Mixed_c))
return Ctlp_Mixed_c;
if (class1 == Ctlp_QuantifierFree_c)
return class2;
if (class2 == Ctlp_QuantifierFree_c)
return class1;
if (class1 == class2)
return class1;
return Ctlp_Mixed_c;
}
/**Function********************************************************************
Synopsis [Returns the class of a formula that is the negation of a formula
of class "class".]
Description [The negation of a mixed (quantifier free, ECTL, ACTL) formula is
mixed (quantifier free, ACTL, ECTL).]
SideEffects []
SeeAlso [Ctlp_CheckClassOfExistentialFormula]
******************************************************************************/
Ctlp_FormulaClass
CtlpNegateFormulaClass(
Ctlp_FormulaClass class_
)
{
switch(class_){
case Ctlp_Mixed_c:
return Ctlp_Mixed_c;
case Ctlp_QuantifierFree_c:
return Ctlp_QuantifierFree_c;
case Ctlp_ECTL_c:
return Ctlp_ACTL_c;
case Ctlp_ACTL_c:
return Ctlp_ECTL_c;
default:
fprintf(vis_stderr, "**Ctlp Error: Unknown formula class\n");
assert(0);
return Ctlp_Mixed_c;
}
}
/**Function********************************************************************
Synopsis [Replaces the smallest important sub-fomula in a w-ACTL
formula by bottom.]
Description [Creates a witness formula for a given w-ACTL formula by
replacing the smallest inpurtant subformula with bottom. This function is
used in the approach to vacuity detection of Beer et al. (CAV97). Formulae
in w-ACTL are guaranteed to have a unique smallest important subformula,
which is defined as follow. If the formula is simple, its operands are not
important. (An exception is made for implications. See
ReplaceSimpleFormula.) Otherwise, the non-simple operand is the important
operand. For (A p U q) or (E p U q), where p and q are both simple, p is the
important operand. For unary formulae, the only child is the important
operand. This function works also for ACTL formulae that are not in w-ACTL,
and for which smallest important subformulae are not unique.
The function picks up a smallest important subformula.]
SideEffects [none]
SeeAlso [ReplaceSimpleFormula]
******************************************************************************/
Ctlp_Formula_t *
Ctlp_FormulaCreateWitnessFormula(
Ctlp_Formula_t *formula)
{
Ctlp_FormulaType formulaType;
Ctlp_Formula_t *rightFormula, *leftFormula;
Ctlp_Formula_t *newLeftFormula, *newRightFormula;
assert(formula != NIL(Ctlp_Formula_t));
if(formula == NIL(Ctlp_Formula_t))
return NIL(Ctlp_Formula_t);
formulaType = Ctlp_FormulaReadType(formula);
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
if (Ctlp_FormulaTestIsQuantifierFree(formula)) {
return ReplaceSimpleFormula(formula);
}
switch (formulaType) {
case Ctlp_AX_c:
case Ctlp_EX_c:
case Ctlp_AG_c:
case Ctlp_EG_c:
case Ctlp_AF_c:
case Ctlp_EF_c:
case Ctlp_NOT_c:
newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
newRightFormula = NIL(Ctlp_Formula_t);
break;
case Ctlp_AU_c:
case Ctlp_EU_c:
/* If both or neither operands are simple, we choose the left one
as important. Deal with special case of converted AG p (E true U p). */
if ((formulaType == Ctlp_EU_c &&
Ctlp_FormulaReadType(leftFormula) == Ctlp_TRUE_c) ||
(Ctlp_FormulaTestIsQuantifierFree(leftFormula) &&
!Ctlp_FormulaTestIsQuantifierFree(rightFormula))) {
newLeftFormula = Ctlp_FormulaDup(leftFormula);
newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
} else {
newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
newRightFormula = Ctlp_FormulaDup(rightFormula);
}
break;
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_THEN_c:
/* Here we know one is not simple */
if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) {
newLeftFormula = Ctlp_FormulaDup(leftFormula);
newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
} else {
newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
newRightFormula = Ctlp_FormulaDup(rightFormula);
}
break;
case Ctlp_XOR_c:
case Ctlp_EQ_c:
newLeftFormula = Ctlp_FormulaDup(leftFormula);
newRightFormula = Ctlp_FormulaDup(rightFormula);
break;
default:
newLeftFormula = NIL(Ctlp_Formula_t);
newRightFormula = NIL(Ctlp_Formula_t);
fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
assert(0);
break;
}
return Ctlp_FormulaCreate(formulaType,newLeftFormula,newRightFormula);
} /* Ctlp_FormulaCreateWitnessFormula */
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Creates a CTL formula with just the type set.]
Description [Calls Ctlp_FormulaCreate with type, and all other fields NULL.]
SideEffects []
SeeAlso [Ctlp_FormulaCreate]
******************************************************************************/
static Ctlp_Formula_t *
FormulaCreateWithType(
Ctlp_FormulaType type)
{
return (Ctlp_FormulaCreate(type, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t)));
}
/**Function********************************************************************
Synopsis [The comparison function for the formula unique table.]
Description [The function takes as parameters two CTL formulae. It compares
the formula type, the left child and the right child, and returns 0 if they
match. Otherwise, it returns -1.]
SideEffects []
SeeAlso [FormulaHash]
******************************************************************************/
static int
FormulaCompare(
const char *key1,
const char *key2)
{
Ctlp_Formula_t *formula1 = (Ctlp_Formula_t *) key1;
Ctlp_Formula_t *formula2 = (Ctlp_Formula_t *) key2;
assert(key1 != NIL(char));
assert(key2 != NIL(char));
if(formula1->type != formula2->type) {
return -1;
}
if(formula1->type == Ctlp_ID_c) {
if(strcmp((char *) (formula1->left), (char *) (formula2->left)) ||
strcmp((char *) (formula1->right), (char *) (formula2->right))) {
return -1;
} else
return 0;
} else {
if(formula1->left != formula2->left)
return -1;
if(formula1->right != formula2->right)
return -1;
if (formula1->type == Ctlp_Cmp_c &&
formula1->compareValue != formula2->compareValue) {
return -1;
}
return 0;
}
}
/**Function********************************************************************
Synopsis [The hash function for the formula unique table.]
Description [The function takes as parameter a CTL formula. If the formula
type is Ctlp_ID_c, st_strhash is used with a concatenation of left and
right children as the key string. Otherwise, something very similar to
st_ptrhash is done.]
SideEffects []
SeeAlso [FormulaCompare]
******************************************************************************/
static int
FormulaHash(
char *key,
int modulus)
{
char *hashString;
int hashValue;
Ctlp_Formula_t *formula = (Ctlp_Formula_t *) key;
if(formula->type==Ctlp_ID_c) {
hashString = util_strcat3((char *) (formula->left), (char *)
(formula->right), "");
hashValue = st_strhash(hashString, modulus);
FREE(hashString);
return hashValue;
}
return (int) ((((unsigned long) formula->left >>2) +
((unsigned long) formula->right >>2)) % modulus);
}
/**Function********************************************************************
Synopsis [Hashes the formula into the unique table.]
Description [The function takes a formula and hashes it and all its
subformulae into a unique table. It returns the unique formula identical to
the formula being hashed. The formula returned will have maximum sharing
with the formulae that are already present in uniqueTable. It returns
NIL(Ctlp_Formula_t) if the formula is NIL(Ctlp_Formula_t).]
SideEffects [If a copy of some subformula of formula is present in
uniqueTable then the copy is substituted for it and the reference count of
the subform
ula is decremented.]
SeeAlso [FormulaCompare]
******************************************************************************/
static Ctlp_Formula_t *
FormulaHashIntoUniqueTable(
Ctlp_Formula_t *formula,
st_table *uniqueTable)
{
Ctlp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight;
if(formula == NIL(Ctlp_Formula_t))
return NIL(Ctlp_Formula_t);
if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
return uniqueFormula;
}
else {
if(formula->type == Ctlp_ID_c) {
st_insert(uniqueTable, formula, formula);
return formula;
}
else {
uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable);
if(uniqueLeft != NIL(Ctlp_Formula_t))
if(uniqueLeft != formula->left) {
CtlpFormulaDecrementRefCount(formula->left);
formula->left = uniqueLeft;
CtlpFormulaIncrementRefCount(formula->left);
}
uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable);
if(uniqueRight != NIL(Ctlp_Formula_t))
if(uniqueRight != formula->right) {
CtlpFormulaDecrementRefCount(formula->right);
formula->right = uniqueRight;
CtlpFormulaIncrementRefCount(formula->right);
}
if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
return uniqueFormula;
}
else {
st_insert(uniqueTable, formula, formula);
return formula;
}
}
}
}
/**Function********************************************************************
Synopsis [Converts the formula tree to a DAG.]
Description [The function recursively builds an existential DAG for the
formula. If a particular sub-formula has been encountered before, the
converted existential sub-formula is pointed to by the field states and it
is returned without creating a new formula.]
SideEffects [We abuse states to store which converted formula an original
formula points to.]
SeeAlso []
******************************************************************************/
static Ctlp_Formula_t *
FormulaConvertToExistentialDAG(
Ctlp_Formula_t *formula)
{
Ctlp_Formula_t *new_;
char *variableNameCopy, *valueNameCopy;
if(formula==NIL(Ctlp_Formula_t))
return NIL(Ctlp_Formula_t);
if(formula->states!=NIL(mdd_t)) {
Ctlp_Formula_t *temp = (Ctlp_Formula_t *) (formula->states);
++(temp->refCount);
return temp;
}
/*
* Recursively convert each subformula.
*/
switch(formula->type) {
case Ctlp_EF_c:
/* EFf --> (E true U f) */
new_ = FormulaCreateWithType(Ctlp_EU_c);
new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->right = FormulaConvertToExistentialDAG(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AX_c:
/* AXf --> !(EX(!f)) */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EX_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AG_c:
/* AGf --> ![(E true U !f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EU_c);
new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->right->left = FormulaConvertToExistentialDAG(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AF_c:
/* AFf --> ![EG(!f)] */
new_ = FormulaCreateWithType(Ctlp_NOT_c);
new_->left = FormulaCreateWithType(Ctlp_EG_c);
new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_AU_c:
/* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->right->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->left->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
new_->left->left->right->left->left = FormulaConvertToExistentialDAG(formula->left); /* f */
new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
new_->left->left->right->right->left = FormulaConvertToExistentialDAG(formula->right); /* g */
new_->dbgInfo.convertedFlag = TRUE;
break;
case Ctlp_ID_c:
/* Make a copy of the name, and create a new formula. */
variableNameCopy = util_strsav((char *)(formula->left));
valueNameCopy = util_strsav((char *)(formula->right));
new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
break;
case Ctlp_THEN_c:
case Ctlp_EX_c:
case Ctlp_EG_c:
case Ctlp_EU_c:
case Ctlp_OR_c:
case Ctlp_AND_c:
case Ctlp_NOT_c:
case Ctlp_XOR_c:
case Ctlp_EQ_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
/* These are already in the correct form. Just convert subformulas. */
new_ = FormulaCreateWithType(formula->type);
new_->left = FormulaConvertToExistentialDAG(formula->left);
new_->right = FormulaConvertToExistentialDAG(formula->right);
break;
default:
fail("Unexpected type");
}
formula->states = (mdd_t *) new_; /*using states as pointer to the converted
formula */
new_->dbgInfo.originalFormula = formula;
return new_;
}
/**Function********************************************************************
Synopsis [Converts an existential formula to forward form.]
Description [Converts an existential formula to forward form. To
convert current formula, it always refer to its parent node and left
child of parent node. Current formula is right child of parent node.
Parent node should be always Ctlp_AND_c and left child of parent node
is already converted. States is used to store a parent pointer
throughout the procedure.]
SideEffects []
SeeAlso []
******************************************************************************/
static void
FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue)
{
Ctlp_Formula_t *parent, *save;
Ctlp_Formula_t *p, *q, *r, *f, *g;
int p_qf, q_qf;
int same_order;
if (formula == NIL(Ctlp_Formula_t))
return;
parent = (Ctlp_Formula_t *)formula->states;
r = parent->left; /* already converted */
/*
* Recursively convert each subformula.
*/
switch(formula->type) {
case Ctlp_EX_c:
/*
** p ^ EXf -> Img(p) ^ f , Img(p) = EY(p)
**
** * *
** / \ / \
** p EX => EY f
** | |
** f p
*/
formula->type = Ctlp_EY_c;
save = formula->left;
formula->left = parent->left;
parent->left = formula;
parent->right = save;
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
break;
case Ctlp_EF_c:
/*
** EFf --> (E true U f)
** p ^ (E true U f) --> FwdU(p, true) ^ f
**
** * *
** / \ / \
** p EF => FwdU f
** | / \
** f p true
*/
formula->type = Ctlp_FwdU_c;
save = formula->left;
formula->right = FormulaCreateWithType(Ctlp_TRUE_c);
formula->left = parent->left;
parent->left = formula;
parent->right = save;
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
break;
case Ctlp_EU_c:
/*
** p ^ (E q U f) --> FwdU(p, q) ^ f
**
** * *
** / \ / \
** p EU => FwdU f
** /\ / \
** q f p q
*/
formula->type = Ctlp_FwdU_c;
save = formula->right;
formula->right = formula->left;
formula->left = parent->left;
parent->left = formula;
parent->right = save;
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
break;
case Ctlp_EG_c:
/*
** p ^ EGq --> FwdG(p, q)
**
** * FwdG
** / \ / \
** p EG => p q
** /
** q
*/
parent->type = Ctlp_FwdG_c;
parent->right = formula->left;
formula->left = NIL(Ctlp_Formula_t);
formula->states = NIL(mdd_t);
Ctlp_FormulaFree(formula);
parent->top = 1;
parent->compareValue = compareValue;
break;
case Ctlp_NOT_c:
if (formula->left->type == Ctlp_NOT_c) {
/*
** * *
** / \ => / \
** r NOT r f
** /
** NOT
** /
** f
*/
parent->right = formula->left->left;
formula->left->left = NIL(Ctlp_Formula_t);
formula->left->states = NIL(mdd_t);
Ctlp_FormulaFree(formula->left);
formula->left = NIL(Ctlp_Formula_t);
formula->states = NIL(mdd_t);
Ctlp_FormulaFree(formula);
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
} else if (formula->left->type == Ctlp_THEN_c) {
/*
** *
** / \
** r NOT
** /
** THEN
** / \
** p q
*/
p = formula->left->left;
q = formula->left->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
if (p_qf && q_qf)
break;
else if (p_qf ||
(p_qf == 0 && q_qf == 0 && !FormulaIsConvertible(q))) {
/*
** !(p -> q) = p * !q
**
** * => * => *
** / \ / \ / \
** r NOT r * * NOT
** / / \ / \ /
** THEN p NOT r p q
** / \ /
** p q q
*/
parent->left = formula->left;
parent->left->type = Ctlp_AND_c;
parent->left->left = r;
parent->left->right = p;
parent->right = formula;
parent->right->left = q;
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
} else {
/*
** !(p -> q) = p * !q
**
** * => * => *
** / \ / \ / \
** r NOT r * * p
** / / \ / \
** THEN p NOT r NOT
** / \ / /
** p q q q
*/
parent->left = formula->left;
parent->left->type = Ctlp_AND_c;
parent->left->left = r;
parent->left->right = formula;
parent->left->right->left = q;
parent->left->right->right = NIL(Ctlp_Formula_t);
parent->right = p;
parent->top = 1;
parent->compareValue = compareValue;
p->states = (mdd_t *)parent;
FormulaConvertToForward(p, compareValue);
}
} else if (formula->left->type == Ctlp_OR_c) {
/*
** !(p + q) = !p * !q
**
** * => * => *
** / \ / \ / \
** r NOT r * * NOT
** / / \ / \ /
** OR NOT NOT r NOT g=q(p)
** / \ / / /
** p q p q f=p(q)
*/
p = formula->left->left;
q = formula->left->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
if (p_qf && q_qf)
break;
else if (p_qf) {
f = p;
g = q;
} else if (q_qf) {
f = q;
g = p;
} else {
if (!FormulaIsConvertible(q)) {
f = p;
g = q;
} else {
f = q;
g = p;
}
}
parent->left = formula->left;
parent->left->type = Ctlp_AND_c;
parent->left->left = r;
parent->left->right = formula;
parent->left->right->left = f;
parent->left->right->right = NIL(Ctlp_Formula_t);
parent->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->left = g;
parent->top = 1;
parent->compareValue = compareValue;
parent->right->states = (mdd_t *)parent;
FormulaConvertToForward(parent->right, compareValue);
} else if (formula->left->type == Ctlp_AND_c) {
/*
** !(p * q) = !p + !q
**
** * *(+) *(+)
** / \ / \ / \
** r NOT => r OR => * *
** / / \ / \ / \
** AND NOT NOT r NOT r NOT
** / \ / / / /
** p q p q p q
*/
p = formula->left->left;
q = formula->left->right;
if (Ctlp_FormulaTestIsQuantifierFree(p) &&
Ctlp_FormulaTestIsQuantifierFree(q)) {
break;
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = formula->left;
parent->left->left = r;
parent->left->right = formula;
parent->left->right->left = p;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = Ctlp_FormulaDup(r);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->right->left = q;
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
} else if (formula->left->type == Ctlp_XOR_c) {
/*
** !(p ^ q) = p * q + !p * !q
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * g * NOT
** / / \ / \ / \ / \ /
** XOR p q NOT NOT r f r NOT g=q(p)
** / \ / / /
** p q p q f=p(q)
*/
p = formula->left->left;
q = formula->left->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
same_order = 1;
if (p_qf && q_qf)
break;
else if (p_qf) {
f = p;
g = q;
} else if (q_qf) {
f = q;
g = p;
} else {
if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
/*
** !(p ^ q) = q * p + !p * !q
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * p * NOT
** / / \ / \ / \ / \ /
** XOR p q NOT NOT r q r NOT q
** / \ / / /
** p q p q p
*/
f = q;
g = p;
same_order = 0;
} else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
/*
** !(p ^ q) = p * q + !q * !p
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * q * NOT
** / / \ / \ / \ / \ /
** XOR p q NOT NOT r p r NOT p
** / \ / / /
** p q p q q
*/
f = p;
g = q;
same_order = 0;
} else {
f = p;
g = q;
}
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = formula;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = f;
parent->left->right = g;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
if (same_order)
parent->right->left->right->left = Ctlp_FormulaDup(f);
else
parent->right->left->right->left = Ctlp_FormulaDup(g);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
if (same_order)
parent->right->right->left = Ctlp_FormulaDup(g);
else
parent->right->right->left = Ctlp_FormulaDup(f);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
} else if (formula->left->type == Ctlp_EQ_c) {
/*
** !(EQ(p, q) = XOR(p, q)
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * g * NOT
** / / \ / \ / \ / \ /
** EQ p NOT NOT q r NOT r f g=q(p)
** / \ / / /
** p q q p f=p(q)
*/
p = formula->left->left;
q = formula->left->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
if (p_qf && q_qf)
break;
else if (p_qf) {
f = p;
g = q;
} else if (q_qf) {
f = q;
g = p;
} else {
if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
/*
** !(EQ(p, q) = XOR(p, q)
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * p * q
** / / \ / \ / \ / \
** EQ p NOT NOT q r NOT r NOT
** / \ / / / /
** p q q p q p
*/
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->left->right->left = q;
parent->left->right = p;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->left->right->left = Ctlp_FormulaDup(p);
parent->right->right = Ctlp_FormulaDup(q);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
} else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
/*
** !(EQ(p, q) = XOR(p, q)
**
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r NOT r * r * * NOT * NOT
** / / \ / \ / \ / / \ /
** EQ p NOT NOT q r p q r q p
** / \ / /
** p q q p
*/
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = p;
parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->right->left = q;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = Ctlp_FormulaDup(q);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->right->left = Ctlp_FormulaDup(p);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
} else {
f = p;
g = q;
}
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->left->right->left = f;
parent->left->right = g;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = Ctlp_FormulaDup(f);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->right->left = Ctlp_FormulaDup(g);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
}
break;
case Ctlp_THEN_c:
/*
** (p -> q) = !p + q
**
** * *(+)
** / \ / \
** r THEN => * *
** / \ / \ / \
** p q r NOT r q
** /
** p
*/
p = formula->left;
q = formula->right;
if (Ctlp_FormulaTestIsQuantifierFree(p) &&
Ctlp_FormulaTestIsQuantifierFree(q)) {
break;
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = formula;
parent->left->type = Ctlp_AND_c;
parent->left->left = r;
parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->right->left = p;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = Ctlp_FormulaDup(r);
parent->right->right = q;
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
case Ctlp_OR_c:
/*
** * *(+)
** / \ / \
** r OR => * *
** / \ / \ / \
** p q r p r q
*/
p = formula->left;
q = formula->right;
if (Ctlp_FormulaTestIsQuantifierFree(p) &&
Ctlp_FormulaTestIsQuantifierFree(q)) {
break;
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = formula;
parent->left->type = Ctlp_AND_c;
parent->left->left = r;
parent->left->right = p;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = Ctlp_FormulaDup(r);
parent->right->right = q;
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
case Ctlp_AND_c:
/*
** * => *
** / \ / \
** r AND AND g=q(p)
** / \ / \
** p q r f=p(q)
*/
p = formula->left;
q = formula->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
if (p_qf && q_qf)
break;
else if (q_qf) {
f = q;
g = p;
} else {
f = p;
g = q;
}
parent->left = parent->right;
parent->left->left = r;
parent->left->right = f;
parent->right = g;
parent->top = 1;
parent->compareValue = compareValue;
g->states = (mdd_t *)parent;
FormulaConvertToForward(g, compareValue);
break;
case Ctlp_XOR_c:
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r XOR r * r * * NOT * g=q(p)
** / \ / \ / \ / \ / / \
** p q q NOT NOT p r f g r NOT
** / / /
** p q f=p(q)
*/
p = formula->left;
q = formula->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
if (p_qf && q_qf)
break;
else if (p_qf) {
f = p;
g = q;
} else if (q_qf) {
f = q;
g = p;
} else {
if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r XOR r * r * * q * p
** / \ / \ / \ / \ / \
** p q q NOT NOT p r NOT r NOT
** / / / /
** p q p q
*/
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->left->right->left = p;
parent->left->right = q;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->left->right->left = Ctlp_FormulaDup(q);
parent->right->right = Ctlp_FormulaDup(p);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
} else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r XOR r * r * * NOT * NOT
** / \ / \ / \ / \ / / \ /
** p q q NOT NOT p r p q r q p
** / /
** p q
*/
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left->type = Ctlp_AND_c;
parent->left->left->left = r;
parent->left->left->right = p;
parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->right->left = q;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = Ctlp_FormulaDup(q);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->right->left = Ctlp_FormulaDup(p);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
} else {
f = p;
g = q;
}
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
parent->left->left->left = r;
parent->left->left->right = f;
parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->left->right->left = g;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
parent->right->left->right->left = Ctlp_FormulaDup(f);
parent->right->right = Ctlp_FormulaDup(g);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
case Ctlp_EQ_c:
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r EQ r * r * * g * NOT
** /\ / \ / \ / \ / \ /
** p q p q NOT NOT r f r NOT g=q(p)
** / / /
** p q f=p(q)
*/
p = formula->left;
q = formula->right;
p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
same_order = 1;
if (p_qf && q_qf)
break;
else if (p_qf) {
f = p;
g = q;
} else if (q_qf) {
f = q;
g = p;
} else {
if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r EQ r * r * * p * NOT
** /\ / \ / \ / \ / \ /
** p q p q NOT NOT r q r NOT q
** / / /
** p q p
*/
f = q;
g = p;
same_order = 0;
} else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
/*
** * *(+) *(+)
** / \ / \ / \
** | | => * * => * *
** | | / \ / \ / \ / \
** r EQ r * r * * q * NOT
** /\ / \ / \ / \ / \ /
** p q p q NOT NOT r p r NOT p
** / / /
** p q q
*/
f = p;
g = q;
same_order = 0;
} else {
f = p;
g = q;
}
}
if (compareValue)
parent->type = Ctlp_OR_c;
parent->left = parent->right;
parent->left->type = Ctlp_AND_c;
parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
parent->left->left->left = r;
parent->left->left->right = f;
parent->left->right = g;
parent->right = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
parent->right->left->left = Ctlp_FormulaDup(r);
parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
if (same_order)
parent->right->left->right->left = Ctlp_FormulaDup(f);
else
parent->right->left->right->left = Ctlp_FormulaDup(g);
parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
if (same_order)
parent->right->right->left = Ctlp_FormulaDup(g);
else
parent->right->right->left = Ctlp_FormulaDup(f);
parent->top = 0;
parent->left->top = 1;
parent->right->top = 1;
parent->left->compareValue = compareValue;
parent->right->compareValue = compareValue;
parent->left->right->states = (mdd_t *)parent->left;
parent->right->right->states = (mdd_t *)parent->right;
FormulaConvertToForward(parent->left->right, compareValue);
FormulaConvertToForward(parent->right->right, compareValue);
break;
case Ctlp_AX_c:
case Ctlp_AG_c:
case Ctlp_AF_c:
case Ctlp_AU_c:
fprintf(vis_stderr,
"** ctl error : invalid node type in converting to forward formula.\n"
);
assert(0);
break;
case Ctlp_ID_c:
case Ctlp_TRUE_c:
case Ctlp_FALSE_c:
break;
default:
fail("Unexpected type");
}
}
/**Function********************************************************************
Synopsis [Inserts compare nodes into forward formula.]
Description [Inserts compare nodes into forward formula.]
SideEffects []
SeeAlso []
******************************************************************************/
static void
FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula,
Ctlp_Formula_t *parent,
int compareValue)
{
Ctlp_Formula_t *new_;
if (formula->top) {
if (!parent) {
new_ = FormulaCreateWithType(Ctlp_Cmp_c);
memcpy((void *)new_, (void *)formula, sizeof(Ctlp_Formula_t));
formula->type = Ctlp_Cmp_c;
formula->left = new_;
formula->right = FormulaCreateWithType(Ctlp_FALSE_c);
formula->compareValue = compareValue;
} else {
new_ = FormulaCreateWithType(Ctlp_Cmp_c);
new_->left = formula;
new_->right = FormulaCreateWithType(Ctlp_FALSE_c);
new_->compareValue = compareValue;
if (parent->left == formula)
parent->left = new_;
else
parent->right = new_;
}
return;
}
FormulaInsertForwardCompareNodes(formula->left, formula, compareValue);
FormulaInsertForwardCompareNodes(formula->right, formula, compareValue);
}
/**Function********************************************************************
Synopsis [Determines which conversion formula is better.]
Description [Determines which conversion formula is better between
init ^ f != FALSE and init ^ !f == FALSE.]
SideEffects []
SeeAlso []
******************************************************************************/
static int
FormulaGetCompareValue(Ctlp_Formula_t *formula)
{
int compareValue;
if (FormulaIsConvertible(formula))
compareValue = 1; /* check whether the result is not FALSE */
else
compareValue = 0; /* check whether the result is FALSE. */
return(compareValue);
}
/**Function********************************************************************
Synopsis [Checks whether a formula can be converted to forward further.]
Description [Checks whether a formula can be converted to forward further.
It returns 1 if it is convertible, and returns 0 if it is not convertible,
and returns 2 if it is partially convertible.]
SideEffects []
SeeAlso []
******************************************************************************/
static int
FormulaIsConvertible(Ctlp_Formula_t *formula)
{
int convertible;
int value1, value2;
if (Ctlp_FormulaTestIsQuantifierFree(formula))
convertible = 1;
else if (formula->type == Ctlp_ID_c)
convertible = 1;
else if (formula->type == Ctlp_EX_c ||
formula->type == Ctlp_EU_c ||
formula->type == Ctlp_EF_c ||
formula->type == Ctlp_EG_c) {
convertible = 1;
} else if (formula->type == Ctlp_NOT_c) {
if (formula->left->type == Ctlp_NOT_c) {
if (formula->left->left->type == Ctlp_EX_c ||
formula->left->left->type == Ctlp_EU_c ||
formula->left->left->type == Ctlp_EF_c ||
formula->left->left->type == Ctlp_EG_c) {
convertible = 1;
} else {
convertible = FormulaIsConvertible(formula->left->left);
}
} else {
if (formula->left->type == Ctlp_EX_c ||
formula->left->type == Ctlp_EU_c ||
formula->left->type == Ctlp_EF_c ||
formula->left->type == Ctlp_EG_c) {
convertible = 0;
} else {
value1 = FormulaIsConvertible(formula->left);
value2 = FormulaIsConvertible(formula->right);
switch (formula->type) {
case Ctlp_AND_c:
case Ctlp_OR_c:
convertible = (value1 & 0x1) * (value2 & 0x1);
break;
case Ctlp_THEN_c:
convertible = value1 * (value2 & 0x1);
break;
default :
convertible = 2;
break;
}
}
}
} else {
value1 = FormulaIsConvertible(formula->left);
value2 = FormulaIsConvertible(formula->right);
switch (formula->type) {
case Ctlp_AND_c:
case Ctlp_OR_c:
convertible = value1 * value2;
break;
case Ctlp_THEN_c:
convertible = (value1 & 0x1) * value2;
break;
default :
convertible = 2;
break;
}
}
return(convertible);
}
/**Function********************************************************************
Synopsis [Replaces a simple formula with bottom.]
Description [This function is used in generating the witness formula from a
w-ACTL formula in Beer's approach to vacuity detection. Replaces a simple
(propositional) subformula with bottom, which is FALSE for even negation
parity and TRUE for odd negation parity. An exception is made when the top
node of the subformula is an implication. In that case, the top node and the
antecedent (left child) are retained in the replacement, while the
consequent (right child) is replaced by bottom.]
SideEffects [none]
SeeAlso [Ctlp_FormulaCreateWitnessFormula]
******************************************************************************/
static Ctlp_Formula_t *
ReplaceSimpleFormula(
Ctlp_Formula_t * formula)
{
Ctlp_Formula_t *newFormula;
assert(formula->negation_parity == Ctlp_Even_c ||
formula->negation_parity == Ctlp_Odd_c);
if (Ctlp_FormulaReadType(formula) == Ctlp_THEN_c) {
Ctlp_Formula_t *leftFormula, *rightFormula;
Ctlp_Formula_t *newLeftFormula, *newRightFormula;
leftFormula = Ctlp_FormulaReadLeftChild(formula);
rightFormula = Ctlp_FormulaReadRightChild(formula);
newLeftFormula = Ctlp_FormulaDup(leftFormula);
newRightFormula = ReplaceSimpleFormula(rightFormula);
return Ctlp_FormulaCreate(Ctlp_THEN_c,newLeftFormula,newRightFormula);
}
fprintf(vis_stderr, "Replacing formula ");
Ctlp_FormulaPrint(vis_stderr, formula);
if (formula->negation_parity == Ctlp_Even_c){
fprintf(vis_stderr, " by FALSE\n");
newFormula = FormulaCreateWithType(Ctlp_FALSE_c);
} else{
fprintf(vis_stderr, " by TRUE\n");
newFormula = FormulaCreateWithType(Ctlp_TRUE_c);
}
newFormula->negation_parity = formula->negation_parity;
return(newFormula);
}