yzh89 / mitl2timed Goto Github PK

After downloading this project, I met some problems when 'make' and running 'mitl2ta'. And after many days of debugging and searching, those problems still confused me, thanks a lot for helping solve them if you can.

Stage 1: make

Though 'make' succeed with no error, some warnings are confusing.

Warning: I cannot understand why use m = in_cache(n) rather than m == in_cache(n) here? As in general, a boolean formula is needed in the if statement. However, mitl2ta didn't work if use m == in_cache(n).

src/rewrt.c:63:8: note: use '==' to turn this assignment into an equality comparison
        if (m = in_cache(n))
              ^
              ==
1 warning generated.

Stage 2: mitl2ta

Here I tried to run ./mitl2ta -f formula where the formula from demo and result.txt. Mainly two errors occurred, Segment Fault and ltl2ba: ERROR in copying CGuard!, saw 'end of formula'. And following are brief results:

Success: Formula (<>_[0,2] a) && (<>_[0,2] b) ((! a) U b) && (<> a)

Segment Fault: Formula []<>_[0,2] a

ltl2ba: ERROR ... : Formula (<> (! <>_[0.0, 2.0] (! b))) && (<> (! <>_[0.0, 2.0] (! a))) []_[0,2] a

Error 1: Segment fault
Debugging shows that at timed.c: 2607 , where tt itself has the probability to be NULL, that caused the Segment fault, so why tt can be NULL, and how to fix this error? Can I simply add a if statement?

  //adjust transitions accordingly
  tt = out->tTrans;
  while(tt->nxt){
    tt = tt->nxt;
  }

Error 2: ltl2ba: ERROR ...
For convenient, use formula []_[0,2] a for debug. Debugging shows that at timed.c: 631, when p->ntyp == 271 && p->lft->ntyp == 263, t1 from t1= build_timed(p->lft); makes t1->tTrans->nxt->cguard->nType == 256, however, 256 is not defined in ltl2ba.h, so when running function CGuard *copy_cguard(CGuard *cg), 256 cannot be matched and error occurred.

default:
        fatal("ERROR in copying CGuard!",(char *)0);
        return (CGuard *)0;

tl_spin: memalloc 91 bytes
tl_spin: memalloc 247 bytes
ltl2ba: ERROR in copying CGuard!, saw 'end of formula'
ltl2ba: []_[0,2] a
--------------------^

After more time debugging, the root cause may at the function(timed.c: 996) merge_event_timed(t1,tA,tB,tOut);, in more detail, root cause may in the for loop (timed.c: 1361) in the function void merge_event_timed(TAutomata *t1, TAutomata *tB, TAutomata *tA, TAutomata *out).

for (int i=0; i < out->stateNum; i++){
//      printf("loop %i ", i);
//      printf("before %i", tB->tTrans->nxt->cguard->nType);
//      printf(" after %i \n", tB->tTrans->nxt->cguard->nType);

      s[tB->stateNum+i].inv = copy_cguard(out->tStates[i].inv);

      s[tB->stateNum+i].input = (unsigned short*) malloc(sizeof(unsigned short)*out->tStates[i].inputNum);

      for (int j=0; j< out->tStates[i].inputNum; j++){
      s[tB->stateNum+i].input[j] = out->tStates[i].input[j];
    }

    create_tstate(&s[tB->stateNum+i], out->tStates[i].tstateId, s[tB->stateNum+i].inv, s[tB->stateNum+i].input, out->tStates[i].inputNum, out->tStates[i].output, out->tStates[i].buchi, NULL);
    if (s[tB->stateNum+i].output == NULLOUT && out->tStates[i].sym == NULL){
      s[tB->stateNum+i].sym = dup_set(t1Sym,3);
      // s[tB->stateNum+i].sym = new_set(3);
      // clear_set(s[tB->stateNum+i].sym , 3);
      // do_merge_sets(s[tB->stateNum+i].sym , tA->tStates[0].sym, t1->tStates[0].sym, 3);
    }else if (s[tB->stateNum+i].output == NULLOUT){
      s[tB->stateNum+i].sym = dup_set(out->tStates[i].sym, 3);
    }
//  if(tB->tTrans->nxt->cguard->nType == 256) printf("%i\n",i);

  }

Unfortunately, I still can not find the exact root cause of this error, so I don't know how to fix it :(