/* -*- C++ -*- * mu_util_dep.h * @(#) part II of the header for Auxiliary routines for the driver * for Murphi verifiers: routines depend on constants declared * in the middle of the compiled program. * RULES_IN_WORLD * * Copyright (C) 1992 - 1999 by the Board of Trustees of * Leland Stanford Junior University. * * License to use, copy, modify, sell and/or distribute this software * and its documentation any purpose is hereby granted without royalty, * subject to the following terms and conditions: * * 1. The above copyright notice and this permission notice must * appear in all copies of the software and related documentation. * * 2. The name of Stanford University may not be used in advertising or * publicity pertaining to distribution of the software without the * specific, prior written permission of Stanford. * * 3. This software may not be called "Murphi" if it has been modified * in any way, without the specific prior written permission of David L. * Dill. * * 4. THE SOFTWARE IS PROVIDED "AS-IS" AND STANFORD MAKES NO * REPRESENTATIONS OR WARRANTIES, EXPRESS OR IMPLIED, BY WAY OF EXAMPLE, * BUT NOT LIMITATION. STANFORD MAKES NO REPRESENTATIONS OR WARRANTIES * OF MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE * USE OF THE SOFTWARE WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS * TRADEMARKS OR OTHER RIGHTS. STANFORD SHALL NOT BE LIABLE FOR ANY * LIABILITY OR DAMAGES WITH RESPECT TO ANY CLAIM BY LICENSEE OR ANY * THIRD PARTY ON ACCOUNT OF, OR ARISING FROM THE LICENSE, OR ANY * SUBLICENSE OR USE OF THE SOFTWARE OR ANY SERVICE OR SUPPORT. * * LICENSEE shall indemnify, hold harmless and defend STANFORD and its * trustees, officers, employees, students and agents against any and all * claims arising out of the exercise of any rights under this Agreement, * including, without limiting the generality of the foregoing, against * any damages, losses or liabilities whatsoever with respect to death or * injury to person or damage to property arising from or out of the * possession, use, or operation of Software or Licensed Program(s) by * LICENSEE or its customers. * * Read the file "license" distributed with these sources, or call * Murphi with the -l switch for additional information. * */ /* * Original Author: Ralph Melton * Extracted from mu_epilog.inc and mu_prolog.inc * by C. Norris Ip * Created: 21 April 93 * * Update: * */ /**************************************** There are 2 groups of declarations: 1) setofrule and sleepset 2) rule_matrix ****************************************/ /**************************************** class setofrule and sleepset require RULES_IN_WORLD ****************************************/ #define BLOCKS_IN_SETOFRULES ( (RULES_IN_WORLD + BITS( BIT_BLOCK ) - 1 ) / \ BITS( BIT_BLOCK )) /* RULES_IN_WORLD gets defined by the generated code. */ /* The extra addition is there so that we round up to the greater block. */ class setofrules { protected: BIT_BLOCK bits[BLOCKS_IN_SETOFRULES]; unsigned NumRules; // Uli: unsigned short -> unsigned int Index(int i) const { return i / BITS( BIT_BLOCK ); }; int Shift(int i) const { return i % BITS( BIT_BLOCK ); }; int Get1(int i) const { return ( bits[ Index(i) ] >> Shift(i) ) & 1; }; void Set1(int i, int val) /* Set bit i to the low bit of val. */ { if ( (val & 1) != 0 ) bits[ Index(i) ] |= ( 1 << Shift(i)); else bits [ Index(i) ] &= ~( 1 << Shift(i)); }; public: // set of rules manipulation friend setofrules interset(setofrules rs1, setofrules rs2); friend setofrules different(setofrules rs1, setofrules rs2); friend bool subset(setofrules rs1, setofrules rs2); // conflict set manipulation friend setofrules conflict(unsigned rule); setofrules() : NumRules(0) { for (int i=0; i