Data Fields
array_t *	flags
int	cnt
int	last
int	nextToLast
int	exBudget
int	exCount
Mc_GSHScheduleType	schedule

Detailed Description

CFile***********************************************************************

FileName [mcGFP.c]

PackageName [mc]

Synopsis [Computation of greatest fixpoints.]

Description [This file contains the functions implementing the Generalized SCC Hull algorithm (GSH) for language emptiness check and for the computation of the states satisfying an EG formula.]

SeeAlso [mcMc.c]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]Struct**********************************************************************

Synopsis [Structure to store disabled operators in GSH.]

Description [Structure to store disabled operators in GSH. A disabled operator is one whose application is known not to cause any progress towards the fixpoint. When all operators are disabled, the computation has converged to the fixpoint. If there are n fairness constraints, the EU operators receive the indices from 0 to n-1, while the one EX is given index n.]

Definition at line 47 of file mcGFP.c.