private void addNextState(final TLCState s,final long fp,final TBGraphNode tnode,final OrderOfSolution oos,final TableauDiskGraph dgraph) throws IOException {
  final boolean[] checkStateRes=oos.checkState(s);
  final int slen=checkStateRes.length;
  final int alen=oos.getCheckAction().length;
  final GraphNode node=dgraph.getNode(fp,tnode.getIndex());
  final int numSucc=node.succSize();
  node.setCheckState(checkStateRes);
  int cnt=0;
  final int nextSize=tnode.nextSize();
  final BitVector checkActionResults=nextSize > 0 ? oos.checkAction(s,s,new BitVector(alen),0) : null;
  for (int i=0; i < nextSize; i++) {
    final TBGraphNode tnode1=tnode.nextAt(i);
    final int tidx1=tnode1.getIndex();
    final long ptr1=dgraph.getPtr(fp,tidx1);
    if (tnode1.isConsistent(s,myTool) && (ptr1 == -1 || !node.transExists(fp,tidx1))) {
      node.addTransition(fp,tidx1,slen,alen,checkActionResults,0,(nextSize - cnt));
      if (ptr1 == -1) {
        dgraph.recordNode(fp,tnode1.getIndex());
        addNextState(s,fp,tnode1,oos,dgraph);
      }
    }
    cnt++;
  }
  cnt=0;
  for (int i=0; i < actions.length; i++) {
    final StateVec nextStates=myTool.getNextStates(actions[i],s);
    final int nextCnt=nextStates.size();
    for (int j=0; j < nextCnt; j++) {
      final TLCState s1=nextStates.elementAt(j);
      if (myTool.isInModel(s1) && myTool.isInActions(s,s1)) {
        final long fp1=s1.fingerPrint();
        final BitVector checkActionRes=oos.checkAction(s,s1,new BitVector(alen),0);
        boolean isDone=dgraph.isDone(fp1);
        for (int k=0; k < tnode.nextSize(); k++) {
          final TBGraphNode tnode1=tnode.nextAt(k);
          final int tidx1=tnode1.getIndex();
          long ptr1=dgraph.getPtr(fp1,tidx1);
          final int total=actions.length * nextCnt * tnode.nextSize();
          if (tnode1.isConsistent(s1,myTool) && (ptr1 == -1 || !node.transExists(fp1,tidx1))) {
            node.addTransition(fp1,tidx1,slen,alen,checkActionRes,0,(total - cnt));
            writer.writeState(s,tnode,s1,tnode1,checkActionRes,0,alen,false,Visualization.DOTTED);
            if (ptr1 == -1) {
              dgraph.recordNode(fp1,tidx1);
              if (isDone) {
                addNextState(s1,fp1,tnode1,oos,dgraph);
              }
            }
          }
          cnt++;
        }
      }
 else {
        cnt++;
      }
    }
  }
  if (numSucc < node.succSize()) {
    node.realign();
    dgraph.addNode(node);
  }
}

private void addNextState ( final TLCState s , final long fp , final TBGraphNode tnode , final OrderOfSolution oos , final TableauDiskGraph dgraph ) throws IOException { final boolean [ ] checkStateRes = oos . checkState ( s ) ; final int slen = checkStateRes . length ; final int alen = oos . getCheckAction ( ) . length ; final GraphNode node = dgraph . getNode ( fp , tnode . getIndex ( ) ) ; final int numSucc = node . succSize ( ) ; node . setCheckState ( checkStateRes ) ; int cnt = 0 ; final int nextSize = tnode . nextSize ( ) ; final BitVector checkActionResults = nextSize > 0 ? oos . checkAction ( s , s , new BitVector ( alen ) , 0 ) : null ; for ( int i = 0 ; i < nextSize ; i ++ ) { final TBGraphNode tnode1 = tnode . nextAt ( i ) ; final int tidx1 = tnode1 . getIndex ( ) ; final long ptr1 = dgraph . getPtr ( fp , tidx1 ) ; if ( tnode1 . isConsistent ( s , myTool ) && ( ptr1 == - 1 || ! node . transExists ( fp , tidx1 ) ) ) { node . addTransition ( fp , tidx1 , slen , alen , checkActionResults , 0 , ( nextSize - cnt ) ) ; if ( ptr1 == - 1 ) { dgraph . recordNode ( fp , tnode1 . getIndex ( ) ) ; addNextState ( s , fp , tnode1 , oos , dgraph ) ; } } cnt ++ ; } cnt = 0 ; for ( int i = 0 ; i < actions . length ; i ++ ) { final StateVec nextStates = myTool . getNextStates ( actions [ i ] , s ) ; final int nextCnt = nextStates . size ( ) ; for ( int j = 0 ; j < nextCnt ; j ++ ) { final TLCState s1 = nextStates . elementAt ( j ) ; if ( myTool . isInModel ( s1 ) && myTool . isInActions ( s , s1 ) ) { final long fp1 = s1 . fingerPrint ( ) ; final BitVector checkActionRes = oos . checkAction ( s , s1 , new BitVector ( alen ) , 0 ) ; boolean isDone = dgraph . isDone ( fp1 ) ; for ( int k = 0 ; k < tnode . nextSize ( ) ; k ++ ) { final TBGraphNode tnode1 = tnode . nextAt ( k ) ; final int tidx1 = tnode1 . getIndex ( ) ; long ptr1 = dgraph . getPtr ( fp1 , tidx1 ) ; final int total = actions . length * nextCnt * tnode . nextSize ( ) ; if ( tnode1 . isConsistent ( s1 , myTool ) && ( ptr1 == - 1 || ! node . transExists ( fp1 , tidx1 ) ) ) { node . addTransition ( fp1 , tidx1 , slen , alen , checkActionRes , 0 , ( total - cnt ) ) ; writer . writeState ( s , tnode , s1 , tnode1 , checkActionRes , 0 , alen , false , Visualization . DOTTED ) ; if ( ptr1 == - 1 ) { dgraph . recordNode ( fp1 , tidx1 ) ; if ( isDone ) { addNextState ( s1 , fp1 , tnode1 , oos , dgraph ) ; } } } cnt ++ ; } } else { cnt ++ ; } } } if ( numSucc < node . succSize ( ) ) { node . realign ( ) ; dgraph . addNode ( node ) ; } }
this method takes care of the case that a new node < < state , tableau > > in the ( state x tableau ) graph is generated after the state itself has been done . done means that the state has been found during safety checking in the state graph already , except that the node < < state , tableau > > not been created . < p > in this case , we will have to generate the state graph successors of the state and create the permutation of all successors with all tableau nodes . < p > hopefully , this case does not occur very frequently because it generates successor nodes .
