source: vis_dev/vis-2.3/src/fsm/fsmFair.c @ 14

Last change on this file since 14 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 30.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [fsmFair.c]
4
5  PackageName [fsm]
6
7  Synopsis    [Implementation of fairness constraints data structure.]
8
9  Description [Implementation of fairness constraints data structure.  The
10  fairness constraint data structure has been defined to allow canonical
11  fairness constraints.  However, presently, only Buchi constraints can be
12  parsed, and the model checker can handle only Buchi constraints.]
13
14  Author      [Tom Shiple and Adnan Aziz and Gitanjali Swamy]
15
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35******************************************************************************/
36
37#include "fsmInt.h"
38
39static char rcsid[] UNUSED = "$Id: fsmFair.c,v 1.28 2003/01/22 18:44:20 jinh Exp $";
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45
46/*---------------------------------------------------------------------------*/
47/* Type declarations                                                         */
48/*---------------------------------------------------------------------------*/
49
50
51/*---------------------------------------------------------------------------*/
52/* Structure declarations                                                    */
53/*---------------------------------------------------------------------------*/
54
55/**Struct**********************************************************************
56
57  Synopsis    [A leaf of the canonical fairness constraint structure.  The name
58  is misleading: this is interpreted as (GF finallyinf + FG globallyInf), a
59  disjunction.]
60
61******************************************************************************/
62typedef struct FairnessConjunctStruct {
63  Ctlp_Formula_t *finallyInf;  /* states to visit infinitely often */
64  Ctlp_Formula_t *globallyInf; /* states to visit almost always */
65} FairnessConjunct_t;
66
67
68/*---------------------------------------------------------------------------*/
69/* Variable declarations                                                     */
70/*---------------------------------------------------------------------------*/
71
72
73/*---------------------------------------------------------------------------*/
74/* Macro declarations                                                        */
75/*---------------------------------------------------------------------------*/
76
77
78/**AutomaticStart*************************************************************/
79
80/*---------------------------------------------------------------------------*/
81/* Static function prototypes                                                */
82/*---------------------------------------------------------------------------*/
83
84static FairnessConjunct_t * FairnessReadConjunct(Fsm_Fairness_t *fairness, int i, int j);
85static mdd_t * FsmObtainStatesSatisfyingFormula(Fsm_Fsm_t *fsm, Ctlp_Formula_t *formula, array_t *careSetArray, Mc_VerbosityLevel verbosity, Mc_DcLevel dcLevel);
86
87/**AutomaticEnd***************************************************************/
88
89
90/*---------------------------------------------------------------------------*/
91/* Definition of exported functions                                          */
92/*---------------------------------------------------------------------------*/
93
94/**Function********************************************************************
95
96  Synopsis    [Returns the fairness constraint of an FSM.]
97
98  Description [Returns the fairness constraint of an FSM.  This is stored as a
99  "canonical fairness constraint", which is a formula of the form (OR_i (AND_j
100  (F-inf S_ij + G-inf T_ij))). Each of the S_ij and T_ij are CTL formulas,
101  representing a set of states in the FSM. F-inf means "globally finally", or
102  "infinitely often"; G-inf means "finally globally" or "almost always".<p>
103
104  Each (AND_j (F-inf S_ij + G-inf T_ij)) is referred to as a "disjunct", and
105  each (F-inf S_ij + G-inf T_ij) is referred to as a "conjunct".  A Streett
106  constraint has just one disjunct.  A Buchi constraint has just one disjunct,
107  and each conjunct of this disjunct has a NULL G-inf condition.<p>
108
109  By default, an FSM is always initialized with a single fairness constraint
110  TRUE, indicating that all states are "accepting".]
111
112  SideEffects []
113
114  SeeAlso     [Fsm_FsmComputeFairStates Fsm_FairnessReadFinallyInfFormula
115  Fsm_FairnessReadGloballyInfFormula]
116
117******************************************************************************/
118Fsm_Fairness_t *
119Fsm_FsmReadFairnessConstraint(
120  Fsm_Fsm_t *fsm)
121{
122  return (fsm->fairnessInfo.constraint);
123}
124
125mdd_t *
126Fsm_FsmReadFairnessStates(Fsm_Fsm_t *fsm)
127{
128   return(fsm->fairnessInfo.states);
129}
130
131
132/**Function********************************************************************
133
134  Synopsis    [Computes the set of fair states of an FSM.]
135
136  Description [Computes the set of fair states of an FSM.  If there is a
137  fairness constraint associated with the FSM, and the fair states have been
138  previously computed, then a copy of the fair states is returned.  If none of
139  the above is true, then the CTL model checker is called to compute the set of
140  fair states, and a copy of this set is returned.  Also, if the CTL model
141  checker is called, information is stored in the FSM for the purpose of
142  debugging CTL formulas in the presence of a fairness constraint.  The second
143  argument is an optional care set array; when this is used, the set of fair
144  states returned is correct on the conjunction of the elements of the care set
145  array.  If careSetArray is set to NIL(mdd_t), it is defaulted to a
146  one-element array containing mdd_one.
147
148  <p> Note that when an FSM is created, by default, there is a single fairness
149  constraint TRUE, indicating that all states are "accepting".  In this case,
150  this function will just return TRUE, which is correct assuming that there are
151  no dead-end states.]
152
153  SideEffects []
154
155  SeeAlso     [Fsm_FsmReadFairnessConstraint]
156
157******************************************************************************/
158mdd_t *
159Fsm_FsmComputeFairStates(
160  Fsm_Fsm_t *fsm,
161  array_t *careSetArray,
162  int verbosity,
163  int dcLevel,
164  Mc_GSHScheduleType schedule,
165  Mc_FwdBwdAnalysis direction,
166  boolean useEarlyTermination)
167{
168  mdd_manager    *mddManager = Fsm_FsmReadMddManager(fsm);
169  Fsm_Fairness_t *constraint = Fsm_FsmReadFairnessConstraint(fsm);
170
171  assert(constraint != NIL(Fsm_Fairness_t));
172
173  if (fsm->fairnessInfo.states != NIL(mdd_t)) {
174    /* Already computed. */
175    return mdd_dup(fsm->fairnessInfo.states);
176  } else {
177    /* Compute from scratch. */
178    mdd_t   *fairStates;
179    array_t *dbgArray = array_alloc(array_t *, 0);
180
181    /* No or trivial fairness constraint */
182    if (FsmFairnessConstraintIsDefault(constraint)) {
183      array_t *onionRings;
184     
185      fairStates = mdd_one(mddManager);
186     
187      onionRings = array_alloc(mdd_t *, 1);
188      array_insert_last(mdd_t *, onionRings, mdd_one(mddManager));
189      array_insert_last(array_t *, dbgArray, onionRings);
190
191      fsm->fairnessInfo.states = mdd_dup(fairStates);
192      fsm->fairnessInfo.dbgArray = dbgArray;
193    } else {
194      mdd_t   *oneMdd = mdd_one(mddManager);
195      array_t *tmpCareSetArray;
196
197      if (careSetArray) {
198        tmpCareSetArray = careSetArray;
199      } else {
200        /* oneMdd is default */
201        tmpCareSetArray = array_alloc(mdd_t *, 0);
202        array_insert_last(mdd_t *, tmpCareSetArray, oneMdd);
203      }
204
205      if (direction == McBwd_c) {
206        mdd_t *initialStates;
207        Mc_EarlyTermination_t *earlyTermination;
208        int fixpoint = 1;
209       
210        if (useEarlyTermination == TRUE) {
211          initialStates = Fsm_FsmComputeInitialStates(fsm);
212          earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
213        } else {
214          initialStates = NIL(mdd_t);
215          earlyTermination = MC_NO_EARLY_TERMINATION;
216        }
217
218        fairStates =
219          Mc_FsmEvaluateEGFormula(fsm,
220                                  oneMdd, NIL(mdd_t), oneMdd,
221                                  constraint, tmpCareSetArray,
222                                  earlyTermination, NIL(array_t),
223                                  Mc_None_c, &dbgArray,
224                                  (Mc_VerbosityLevel) verbosity,
225                                  (Mc_DcLevel) dcLevel,
226                                  &fixpoint, schedule);
227        if (useEarlyTermination == TRUE) {
228          Mc_EarlyTerminationFree(earlyTermination);
229          mdd_free(initialStates);
230        }
231        if (!fixpoint) {
232          int i;
233          array_t *mddArray;
234          arrayForEachItem(array_t *, dbgArray, i, mddArray) {
235            mdd_array_free(mddArray);
236          }
237          array_free(dbgArray);
238        } else {
239          fsm->fairnessInfo.states = mdd_dup(fairStates);
240          fsm->fairnessInfo.dbgArray = dbgArray;
241        }
242      } else {
243        fairStates =
244          Mc_FsmEvaluateEHFormula(fsm,
245                                  oneMdd, NIL(mdd_t), oneMdd,
246                                  constraint, tmpCareSetArray,
247                                  MC_NO_EARLY_TERMINATION, NIL(array_t),
248                                  Mc_None_c, NIL(array_t *),
249                                  (Mc_VerbosityLevel) verbosity,
250                                  (Mc_DcLevel) dcLevel,
251                                  NIL(boolean), schedule);
252        array_free(dbgArray);
253      }
254      if (tmpCareSetArray != careSetArray)
255        array_free(tmpCareSetArray);
256      mdd_free(oneMdd);
257    }
258
259    return fairStates;
260  }/* compute from scratch*/
261}
262
263
264/**Function********************************************************************
265
266  Synopsis    [Reads the finallyInf component of a leaf of a canonical fairness
267  constraint.]
268
269  Description [Reads the finallyInf component of the jth conjunct of the ith
270  disjunct of a canonical fairness constraint (i and j start counting from
271  0). This is CTL formula representing a set of states of an FSM; this formula
272  is not necessarily in existential normal form. If there is no finallyInf
273  component at this location, then a NULL formula is returned.  It is assumed
274  that i and j are within bounds.]
275
276  SideEffects []
277
278  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
279  Fsm_FairnessReadFinallyInfMdd]
280
281******************************************************************************/
282Ctlp_Formula_t *
283Fsm_FairnessReadFinallyInfFormula(
284  Fsm_Fairness_t *fairness,
285  int i,
286  int j)
287{
288  FairnessConjunct_t *conjunct = FairnessReadConjunct(fairness, i, j);
289  return (conjunct->finallyInf);
290}
291
292
293/**Function********************************************************************
294
295  Synopsis    [Reads the globallyInf component of a leaf of a canonical fairness
296  constraint.]
297
298  Description [Reads the globallyInf component of the jth conjunct of the ith
299  disjunct of a canonical fairness constraint (i and j start counting from
300  0). This is CTL formula representing a set of states of an FSM; this formula
301  is not necessarily in existential normal form. If there is no globallyInf
302  component at this location, then a NULL formula is returned.  It is assumed
303  that i and j are within bounds.]
304
305  SideEffects []
306
307  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadFinallyInfFormula
308  Fsm_FairnessReadGloballyInfMdd]
309
310******************************************************************************/
311Ctlp_Formula_t *
312Fsm_FairnessReadGloballyInfFormula(
313  Fsm_Fairness_t *fairness,
314  int i,
315  int j)
316{
317  FairnessConjunct_t *conjunct = FairnessReadConjunct(fairness, i, j);
318  return (conjunct->globallyInf);
319}
320
321/**Function********************************************************************
322
323  Synopsis [Obtains a copy of the MDD of the finallyInf component of a leaf of
324  a canonical fairness constraint.]
325
326  Description [Obtains a copy of the MDD of the finallyInf component of the
327  jth conjunct of the ith disjunct of a canonical fairness constraint (i and j
328  start counting from 0). This MDD represents the set of FSM states which
329  satisfy the finallyInf formula.  This set is guaranteed to be correct on the
330  set of reachable states.  If there is no finallyInf component at this
331  location, then a NULL MDD is returned.  It is assumed that i and j are
332  within bounds.  The first time this function is called with the given data,
333  the CTL model checker is called to compute the set of states (with all
334  states fair, and no fairness constraint); additional calls take constant
335  time. It is the responsibililty of the calling function to free the returned
336  mdd.]
337
338  SideEffects []
339
340  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadFinallyInfFormula
341  Fsm_FairnessReadGloballyInfMdd]
342
343******************************************************************************/
344mdd_t *
345Fsm_FairnessObtainFinallyInfMdd(
346  Fsm_Fairness_t *fairness,
347  int i,
348  int j,
349  array_t *careSetArray,
350  Mc_DcLevel dcLevel)
351{
352  Ctlp_Formula_t *formula = Fsm_FairnessReadFinallyInfFormula(fairness, i, j);
353  /* hard code verbosity to Mc_VerbosityNone */
354  return(FsmObtainStatesSatisfyingFormula(fairness->fsm, formula, careSetArray,
355                                          McVerbosityNone_c, dcLevel));
356}
357
358
359/**Function********************************************************************
360
361  Synopsis [Obtains a copy of the MDD of the globallyInf component of a leaf of
362  a canonical fairness constraint.]
363
364  Description [Obtains a copy of the MDD of the globallyInf component of the
365  jth conjunct of the ith disjunct of a canonical fairness constraint (i and j
366  start counting from 0). This MDD represents the set of FSM states which
367  satisfy the globallyInf formula.  This set is guaranteed to be correct on
368  the set of reachable states.  If there is no globallyInf component at this
369  location, then a NULL MDD is returned.  It is assumed that i and j are
370  within bounds. The first time this function is called with the given data,
371  the CTL model checker is called to compute the set of states (with all
372  states fair, and no fairness constraint); additional calls take constant
373  time. It is the responsibililty of the calling function to free the returned
374  mdd.]
375
376  SideEffects []
377
378  SeeAlso [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
379  Fsm_FairnessReadFinallyInfMdd]
380
381******************************************************************************/
382mdd_t *
383Fsm_FairnessObtainGloballyInfMdd(
384  Fsm_Fairness_t *fairness,
385  int i,
386  int j,
387  array_t *careSetArray,
388  Mc_DcLevel dcLevel)
389{
390  Ctlp_Formula_t *formula = Fsm_FairnessReadGloballyInfFormula(fairness, i, j);
391  /* hard code verbosity to Mc_VerbosityNone */
392  return(FsmObtainStatesSatisfyingFormula(fairness->fsm, formula, careSetArray,
393                                          McVerbosityNone_c, dcLevel));
394
395}
396
397
398/**Function********************************************************************
399
400  Synopsis [Returns TRUE if fairness constraint is of type Streett.]
401
402  Description [Returns TRUE if fairness constraint is of type Streett, else
403  FALSE.  A Streett fairness constraint is a canonical fairness constraint,
404  with one disjunct.]
405
406  SideEffects []
407
408  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessTestIsBuchi]
409
410******************************************************************************/
411boolean
412Fsm_FairnessTestIsStreett(
413  Fsm_Fairness_t *fairness)
414{
415  return (array_n(fairness->disjunctArray) == 1);
416}
417
418
419/**Function********************************************************************
420
421  Synopsis [Returns TRUE if fairness constraint is of type Buchi].
422
423  Description [Returns TRUE if fairness constraint is of type Buchi, else
424  FALSE.  A Buchi fairness constraint is a canonical fairness constraint, with
425  one disjunct, where each conjunct has a NULL G-inf condition.  Note that a
426  Buchi constraint is also a Streett constraint.]
427
428  SideEffects []
429
430  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessTestIsStreet]
431
432******************************************************************************/
433boolean
434Fsm_FairnessTestIsBuchi(
435  Fsm_Fairness_t *fairness)
436{
437  if (array_n(fairness->disjunctArray) != 1) {
438    return (FALSE);
439  }
440  else {
441    int      j;
442    array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, 0);
443
444    for (j = 0; j < array_n(disjunct); j++) {
445      FairnessConjunct_t *conjunct = array_fetch(FairnessConjunct_t *,
446                                                 disjunct, j);
447      if (conjunct->globallyInf != NIL(Ctlp_Formula_t)) {
448        return (FALSE);
449      }
450    }
451    return (TRUE);
452  }
453}
454
455
456/**Function********************************************************************
457
458  Synopsis    [Returns the number of disjuncts of a canonical fairness
459  constraint.]
460
461  SideEffects []
462
463  SeeAlso     [Fsm_FsmReadFairnessConstraint
464  Fsm_FairnessReadNumConjunctsOfDisjunct]
465
466******************************************************************************/
467int
468Fsm_FairnessReadNumDisjuncts(
469  Fsm_Fairness_t *fairness)
470{
471  return (array_n(fairness->disjunctArray));
472}
473
474
475/**Function********************************************************************
476
477  Synopsis [Returns the number of conjuncts of the ith disjunct of a canonical
478  fairness constraint.]
479
480  SideEffects []
481
482  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadNumDisjuncts]
483
484******************************************************************************/
485int
486Fsm_FairnessReadNumConjunctsOfDisjunct(
487  Fsm_Fairness_t *fairness,
488  int i)
489{
490  array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, i);
491
492  return (array_n(disjunct));
493}
494
495
496/**Function********************************************************************
497
498  Synopsis    [Returns the fair CTL debugging information of an FSM.]
499
500  Description [Returns the fair CTL debugging information of an FSM.
501  Currently, the fairness constraints are limited to Buchi constraints. The
502  return value is an array of array_t* of mdd_t*.  The returned array is of
503  length k, where k is the number of Buchi constraints.  The ith element of
504  the returned array is an array of MDDs giving the sequence of state sets
505  that can reach the ith Buchi constraint.  In particular, the jth MDD of the
506  ith array is the set of states that can reach the ith Buchi set in j or
507  fewer steps (the 0th MDD is the ith Buchi set itself).]
508
509  SideEffects []
510
511  SeeAlso     [Fsm_FsmReadFairnessConstraint]
512
513******************************************************************************/
514array_t *
515Fsm_FsmReadDebugArray(Fsm_Fsm_t *fsm)
516{
517  return (fsm->fairnessInfo.dbgArray);
518}
519
520
521/**Function********************************************************************
522
523  Synopsis    [Create and Update the fairness constraint of the FSM.]
524
525  Description [Given the FSM and an array of CTL formula, build the buechi
526  fairness constraints, and update.]
527
528  SideEffects []
529
530  SeeAlso     [Fsm_FsmReadFairnessConstraint]
531
532******************************************************************************/
533void
534Fsm_FsmFairnessUpdate(
535  Fsm_Fsm_t *fsm,
536  array_t *formulaArray)
537{
538    Fsm_Fairness_t *fairness = FsmFairnessAlloc(fsm);
539    int j;
540    /*
541     * Interpret the array of CTL formulas as a set of Buchi conditions.
542     * Hence, create a single disjunct, consisting of k conjuncts, where k is
543     * the number of CTL formulas read in.  The jth conjunct has the jth
544     * formula as its finallyInf component, and NULL as its globallyInf
545     * component.
546     */
547   
548    for (j = 0; j < array_n(formulaArray); j++) {
549      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);
550
551      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
552    }
553
554    /*
555     * Remove any existing fairnessInfo associated with the FSM, and update
556     * the fairnessInfo.constraint with the new fairness just read.
557     */
558    FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t));
559}
560
561
562/*---------------------------------------------------------------------------*/
563/* Definition of internal functions                                          */
564/*---------------------------------------------------------------------------*/
565
566/**Function********************************************************************
567
568  Synopsis    [Create a default fairness constraint.]
569
570  Description [Create a default fairness constraint containing a single
571  formula, TRUE, indicating that all states are "accepting".]
572
573  SideEffects []
574
575  SeeAlso     [Fsm_FsmReadFairnessConstraint]
576
577******************************************************************************/
578Fsm_Fairness_t *
579FsmFsmCreateDefaultFairnessConstraint(
580  Fsm_Fsm_t *fsm)
581{
582  Fsm_Fairness_t *fairness    = FsmFairnessAlloc(fsm);
583  Ctlp_Formula_t *trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c,
584                                                   NIL(Ctlp_Formula_t),
585                                                   NIL(Ctlp_Formula_t));
586
587  FsmFairnessAddConjunct(fairness, trueFormula, NIL(Ctlp_Formula_t), 0, 0);
588  return fairness;
589}
590
591
592/**Function********************************************************************
593
594  Synopsis    [See whether the fairness constraint is the default one]
595
596  Description [See if the fairness constraint is the default one, which implies
597  that all states are accepting.]
598
599  SideEffects []
600
601  SeeAlso     [FsmFsmCreateDefaultFairnessConstraint]
602
603******************************************************************************/
604boolean
605FsmFairnessConstraintIsDefault(
606  Fsm_Fairness_t *fairness)
607{
608  array_t            *disjuncts;
609  array_t            *conjuncts;
610  FairnessConjunct_t *leaf;
611  Ctlp_Formula_t     *tautology;
612  boolean            result;
613 
614  /* one disjunct */
615  disjuncts = fairness->disjunctArray;
616  if(array_n(disjuncts) !=  1)
617    return FALSE;
618
619  /* one conjunct */
620  conjuncts = array_fetch(array_t *, disjuncts, 0);
621  if(array_n(conjuncts) != 1)
622    return FALSE;
623
624  /* set to (GF TRUE * FG NULL) */
625  leaf = array_fetch(FairnessConjunct_t *, conjuncts, 0);
626  if(leaf->globallyInf != NIL(Ctlp_Formula_t))
627    return FALSE;
628
629  tautology = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(Ctlp_Formula_t),
630                                 NIL(Ctlp_Formula_t));
631  result = Ctlp_FormulaIdentical(tautology, leaf->finallyInf);
632  Ctlp_FormulaFree(tautology);
633
634  return result;
635}
636
637
638/**Function********************************************************************
639
640  Synopsis    [Frees a fairness constraint.]
641
642  Description [Frees all the memory associated with a fairness constraint,
643  including the underlying CTL formulas.]
644
645  SideEffects []
646
647  SeeAlso     [FsmFairnessAlloc]
648
649******************************************************************************/
650void
651FsmFairnessFree(
652  Fsm_Fairness_t *fairness)
653{
654  int i;
655
656  for (i = 0; i < array_n(fairness->disjunctArray); i++) {
657    int j;
658    array_t *disjunct = array_fetch(array_t *, fairness->disjunctArray, i);
659
660    for (j = 0; j < array_n(disjunct); j++) {
661      FairnessConjunct_t *conjunct = array_fetch(FairnessConjunct_t *,
662                                                 disjunct, j);
663      Ctlp_FormulaFree(conjunct->finallyInf);
664      Ctlp_FormulaFree(conjunct->globallyInf);
665      FREE(conjunct);
666    }
667    array_free(disjunct);
668  }
669  array_free(fairness->disjunctArray);
670  FREE(fairness);
671}
672
673
674/**Function********************************************************************
675
676  Synopsis    [Allocates a fairness constraint.]
677
678  Description [Allocates a fairness constraint.  Sets the FSM pointer, and
679  allocates a disjunct array containing 0 elements.]
680
681  SideEffects []
682
683  SeeAlso     [FsmFairnessFree FsmFairnessAddConjunct]
684
685******************************************************************************/
686Fsm_Fairness_t *
687FsmFairnessAlloc(Fsm_Fsm_t *fsm)
688{
689  Fsm_Fairness_t *fairness = ALLOC(Fsm_Fairness_t, 1);
690
691  fairness->fsm           = fsm;
692  fairness->disjunctArray = array_alloc(array_t *, 0);
693
694  return fairness;
695}
696
697
698/**Function********************************************************************
699
700  Synopsis    [Adds a conjunct to a fairness constraint.]
701
702  Description [Adds a conjunct to a fairness constraint. i and j must not be
703  negative; otherwise, there is no restriction on their values.  i and j start
704  counting from 0.  Note that it is possible to create a 2-D array with
705  "holes" in it, although this is probably not desirable.  If holes are
706  created, they are zeroed out.]
707
708  SideEffects []
709
710  SeeAlso     [FsmFairnessAlloc]
711
712******************************************************************************/
713void
714FsmFairnessAddConjunct(
715  Fsm_Fairness_t *fairness,
716  Ctlp_Formula_t *finallyInf,
717  Ctlp_Formula_t *globallyInf,
718  int             i,
719  int             j)
720{
721  int k;
722  array_t *disjunct;
723  int numConjuncts;
724  int                 numDisjuncts = array_n(fairness->disjunctArray);
725  FairnessConjunct_t *conjunct     = ALLOC(FairnessConjunct_t, 1);
726
727  assert((i >= 0) && (j >= 0));
728
729  /* Get the array for row i. */
730  if (i >= numDisjuncts) {
731    /*
732     * i is out of range.  Create a new disjunct, add it to the array, and
733     * zero out the intervening entries.
734     */
735    disjunct = array_alloc(FairnessConjunct_t *, 0);
736
737    /* Note that the array is dynamically extended. */
738    array_insert(array_t *, fairness->disjunctArray, i, disjunct);
739
740    /* Zero out the holes just created (if any). */
741    for (k = numDisjuncts; k < i; k++) {
742      array_insert(array_t *, fairness->disjunctArray, k, NIL(array_t));
743    }
744  }
745  else {
746    /*
747     * i is in range.  However, there may not be a non-NIL array at entry i
748     * yet.
749     */
750    disjunct = array_fetch(array_t *, fairness->disjunctArray, i);
751    if (disjunct == NIL(array_t)) {
752      disjunct = array_alloc(FairnessConjunct_t *, 0);
753      array_insert(array_t *, fairness->disjunctArray, i, disjunct);
754    }
755  }
756
757  /*
758   * Fill in the conjunct, and add it to the jth position of the ith row.  If
759   * holes are created, then zero them out.
760   */
761  conjunct->finallyInf  = finallyInf;
762  conjunct->globallyInf = globallyInf;
763
764  array_insert(FairnessConjunct_t *, disjunct, j, conjunct);
765  numConjuncts = array_n(disjunct);
766  for (k = numConjuncts; k < j; k++) {
767    array_insert(FairnessConjunct_t *, disjunct, k, NIL(FairnessConjunct_t));
768  }
769}
770
771
772/**Function********************************************************************
773
774  Synopsis    [Updates the fairnessInfo of an FSM.]
775
776  Description [Updates the fairnessInfo of an FSM with the supplied arguments.
777  If any of the existing fields are currently non-NULL, then first frees
778  them. DbgArray is assumed to be an array of arrays of mdd_t's.]
779
780  SideEffects []
781
782******************************************************************************/
783void
784FsmFsmFairnessInfoUpdate(
785  Fsm_Fsm_t *fsm,
786  mdd_t *states,
787  Fsm_Fairness_t *constraint,
788  array_t *dbgArray)
789{
790  array_t *oldDbgArray = fsm->fairnessInfo.dbgArray;
791
792  if (fsm->fairnessInfo.states != NIL(mdd_t)){
793    mdd_free(fsm->fairnessInfo.states);
794  }
795  fsm->fairnessInfo.states = states;
796
797  if (fsm->fairnessInfo.constraint != NIL(Fsm_Fairness_t)) {
798    FsmFairnessFree(fsm->fairnessInfo.constraint);
799  }
800  fsm->fairnessInfo.constraint = constraint;
801
802  if (oldDbgArray != NIL(array_t)) {
803    int i;
804    for (i = 0; i < array_n(oldDbgArray); i++) {
805      array_t *mddArray = array_fetch(array_t *, oldDbgArray, i);
806      mdd_array_free(mddArray);
807    }
808    array_free(oldDbgArray);
809  }
810  fsm->fairnessInfo.dbgArray = dbgArray;
811}
812
813
814
815/*---------------------------------------------------------------------------*/
816/* Definition of static functions                                            */
817/*---------------------------------------------------------------------------*/
818
819/**Function********************************************************************
820
821  Synopsis    [Reads a leaf of a canonical fairness constraint.]
822
823  Description [Reads the the jth conjunct of the ith disjunct of a canonical
824  fairness constraint.  It is assumed that i and j are within bounds.]
825
826  SideEffects []
827
828  SeeAlso     [Fsm_FsmReadFairnessConstraint Fsm_FairnessReadGloballyInfFormula
829  Fsm_FairnessReadFinallyInfMdd]
830
831******************************************************************************/
832static FairnessConjunct_t *
833FairnessReadConjunct(
834  Fsm_Fairness_t *fairness,
835  int i,
836  int j)
837{
838  array_t            *disjunct;
839  FairnessConjunct_t *conjunct;
840
841  assert((i >= 0) && (i < array_n(fairness->disjunctArray)));
842  disjunct = array_fetch(array_t *, fairness->disjunctArray, i);
843
844  assert((j >= 0) && (j < array_n(disjunct)));
845  conjunct = array_fetch(FairnessConjunct_t *, disjunct, j);
846
847  return conjunct;
848}
849
850
851/**Function********************************************************************
852
853  Synopsis    [Obtains the set of states satisfying a formula.]
854
855  Description [Returns a copy of the set of states satisfying a CTL formula,
856  in the context of an FSM.  If this set has already been computed for this
857  formula, then a copy is returned.  Otherwise, the CTL model checker is
858  called on the existential normal form of the formula, with all states fair,
859  and no fairness constraint.  The result is guaranteed correct on reachable
860  states.  If formula is NULL, then a NULL MDD is returned.]
861
862  SideEffects []
863
864  SeeAlso     [Fsm_FairnessObtainFinallyInfMdd Fsm_FairnessObtainGloballyInfMdd]
865
866******************************************************************************/
867static mdd_t *
868FsmObtainStatesSatisfyingFormula(
869  Fsm_Fsm_t      *fsm,
870  Ctlp_Formula_t *formula,
871  array_t *careSetArray,
872  Mc_VerbosityLevel verbosity,
873  Mc_DcLevel dcLevel)
874{
875  if (formula == NIL(Ctlp_Formula_t)) {
876    return (NIL(mdd_t));
877  }
878  else {
879    mdd_t *stateSet = Ctlp_FormulaObtainStates(formula);
880
881    if (stateSet != NIL(mdd_t)) {
882      return stateSet;
883    }
884    else {
885      mdd_t          *result;
886      mdd_manager    *mddManager  = Fsm_FsmReadMddManager(fsm);
887      mdd_t          *oneMdd      = mdd_one(mddManager);
888      Ctlp_Formula_t *convFormula =
889                        Ctlp_FormulaConvertToExistentialForm(formula);
890
891      /* Note that Mc_FsmEvaluateFormula returns a copy of the MDD. */
892      result = Mc_FsmEvaluateFormula(fsm, convFormula, oneMdd,
893                                     NIL(Fsm_Fairness_t),
894                                     careSetArray,
895                                     MC_NO_EARLY_TERMINATION,
896                                     NIL(Fsm_HintsArray_t),
897                                     Mc_None_c, verbosity, dcLevel, 0,
898                                     McGSH_EL_c);
899      mdd_free(oneMdd);
900
901      /*
902       * We must make a copy of the MDD for the return value.
903       */
904      Ctlp_FormulaSetStates(formula, result);
905      stateSet = mdd_dup(result);
906
907      Ctlp_FormulaFree(convFormula);
908
909      return stateSet;
910    }
911  }
912}
Note: See TracBrowser for help on using the repository browser.