QSDL-TL/TLFormulaALWAYS.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
/*
 * File:    TLFormulaALWAYS.cc
 * Project: QUEST
 * Author:  Marc Diefenbruch, Axel M Hirche
 * Date:    (C) 1997, 1998 University of Essen, Germany
 */

#include "SCL/SCStream.h"

#include "TLFormulaALWAYS.h"
#include "TLFormulaEVENTUALLY.h"
#include "TLFormulaV_OPER.h"
#include "TLFormulaFALSE.h"

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

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


TLFormulaALWAYS::~TLFormulaALWAYS (void)
{
  /* empty */
}


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


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

  if (simplifyFormulae)
  {
    if (rightOperand->Operator() == ALWAYS)
    {
      return rightOperand->Rewrite();             // [][]...[]a  <->  []a
    }

    if (rightOperand->Operator() == EVENTUALLY)
    {
      TLFormulaEVENTUALLY* tmpRight = (TLFormulaEVENTUALLY*) rightOperand;

      if (tmpRight->RightOperand()->Operator() == ALWAYS)
      {
        return rightOperand->Rewrite();           // []<>[]...[]<>[]a  <->  <>[]a
      }
    }
  }

  if (TLFormula::partialRewrite)                  // Don´t rewrite it.
  {
    return new TLFormulaALWAYS (rightOperand->Rewrite(), false);
  }
  else                                            // Rewrite it.
  {
    return new TLFormulaV_OPER (new TLFormulaFALSE(),
                                rightOperand->Rewrite());
  }
}


TLFormula* TLFormulaALWAYS::PushNegations (SCBoolean doIt) const
{
  if (doIt)
    return new TLFormulaEVENTUALLY (rightOperand->PushNegations(doIt),
                                    false);
  else
    return new TLFormulaALWAYS(rightOperand->PushNegations(doIt),
                               false);
}


SCNatural TLFormulaALWAYS::GetPrecedenceLevel (void) const
{
  return PREC_LEVEL_2;
}