static void addTemporalLevelConstraintToConstants(HashSet params,SetOfLevelConstraints constrs){
  Iterator iter=params.iterator();
  while (iter.hasNext()) {
    LevelNode node=(LevelNode)iter.next();
    if (node.getKind() == ConstantDeclKind) {
      constrs.put(node,Levels[ActionLevel]);
    }
    ;
  }
}

static void addTemporalLevelConstraintToConstants ( HashSet params , SetOfLevelConstraints constrs ) { Iterator iter = params . iterator ( ) ; while ( iter . hasNext ( ) ) { LevelNode node = ( LevelNode ) iter . next ( ) ; if ( node . getKind ( ) == ConstantDeclKind ) { constrs . put ( node , Levels [ ActionLevel ] ) ; } ; } }
the following method adds to constrs a level constaint that the level of c < temporallevel for every declared constant c in the set params of nodes . * called when level checking an assume statement or an assume / prove to prevent a declared constant that appears in it from being instantiated by a temporal formula . added by ll on 1 mar 2009
