QSDL-TL/TLFormulaUNTIL.cpp at master · Diefenbruch/QSDL-TL · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
/*
 * File:    TLFormulaUNTIL.cc
 * Project: QUEST
 * Author:  Marc Diefenbruch, Axel M. Hirche
 * Date:    (C) 1997, 1998 University of Essen, Germany
 */

#include "TLFormulaUNTIL.h"
#include "TLFormulaV_OPER.h"
#include "TLFormulaWAITFOR.h"
#include "TLFormulaTRUE.h"
#include "TLFormulaFALSE.h"
//#include "SCL/SCListIter.h"
#include "TLFormulaSet.h"

#if _TL_INLINING_ == 0
#include "TLFormulaUNTIL.inl.h"
#endif

#if _SC_DMALLOC
  #include <dmalloc.h>
#endif

TLFormulaUNTIL::~TLFormulaUNTIL (void)
{
  /* void */
}


TLFormula* TLFormulaUNTIL::GetCopy (void) const
{
  return new TLFormulaUNTIL (this);
}


TLFormula* TLFormulaUNTIL::Rewrite (void) const
{
  assert (leftOperand);
  assert (rightOperand);

  if (simplifyFormulae)
  {
    if (rightOperand->Operator() == T)
    {
      return new TLFormulaTRUE();                   // a U T <-> T
    }

    if (rightOperand->Operator() == F)
    {
      return new TLFormulaFALSE();                  // a U F <-> F
    }

    if (rightOperand->Operator() == UNTIL)
    {
      assert (((TLFormulaUNTIL*)rightOperand)->RightOperand());
      assert (((TLFormulaUNTIL*)rightOperand)->LeftOperand());

      if (*((TLFormulaUNTIL*)rightOperand)->LeftOperand() == *leftOperand)
      {
        return rightOperand->Rewrite();             // a U (a U b) <-> a U b
      }
    }

    if (leftOperand->Operator() == UNTIL)
    {
      assert (((TLFormulaUNTIL*)leftOperand)->RightOperand());
      assert (((TLFormulaUNTIL*)leftOperand)->LeftOperand());

      if (*((TLFormulaUNTIL*)leftOperand)->RightOperand() == *rightOperand)
      {
        return leftOperand->Rewrite();             // (a U b) b <-> a U b
      }
    }

    if (rightOperand->Operator() == WAITFOR)
    {
      TLFormulaWAITFOR* tmpRight = (TLFormulaWAITFOR*) rightOperand;

      if (*tmpRight->LeftOperand() == *leftOperand)
      {
        return new TLFormulaWAITFOR (leftOperand->Rewrite(),
                                     tmpRight->RightOperand()->Rewrite());
                                                  // a U (a W b)  <-> a W b
      }
    }

    if (leftOperand->Operator() == WAITFOR)
    {
      TLFormulaWAITFOR* tmpLeft = (TLFormulaWAITFOR*) leftOperand;

      if (*tmpLeft->RightOperand() == *rightOperand)
      {
        return new TLFormulaUNTIL (tmpLeft->LeftOperand()->Rewrite(),
                                   rightOperand->Rewrite());
                                                  // (a W b) U b  <-> a U b
      }
    }
  }

  return new TLFormulaUNTIL (leftOperand->Rewrite(),
                             rightOperand->Rewrite());
}


TLFormula* TLFormulaUNTIL::PushNegations (SCBoolean doIt) const
{
  if (doIt)
    return new TLFormulaV_OPER (leftOperand->PushNegations (doIt),
                                rightOperand->PushNegations (doIt));
  else
    return new TLFormulaUNTIL (leftOperand->PushNegations (doIt),
                               rightOperand->PushNegations (doIt));
}


SCNatural TLFormulaUNTIL::GetPrecedenceLevel (void) const
{
  return PREC_LEVEL_1;
}


SCBoolean TLFormulaUNTIL::HasAcceptanceStateSet (void) const
{
  return true;
}