libutap  0.93
Uppaal Timed Automata Parser
expression.cpp
Go to the documentation of this file.
1 // -*- mode: C++; c-file-style: "stroustrup"; c-basic-offset: 4; indent-tabs-mode: nil; -*-
2 
3 /* libutap - Uppaal Timed Automata Parser.
4  Copyright (C) 2011-2018 Aalborg University.
5  Copyright (C) 2002-2006 Uppsala University and Aalborg University.
6 
7  This library is free software; you can redistribute it and/or
8  modify it under the terms of the GNU Lesser General Public License
9  as published by the Free Software Foundation; either version 2.1 of
10  the License, or (at your option) any later version.
11 
12  This library is distributed in the hope that it will be useful, but
13  WITHOUT ANY WARRANTY; without even the implied warranty of
14  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15  Lesser General Public License for more details.
16 
17  You should have received a copy of the GNU Lesser General Public
18  License along with this library; if not, write to the Free Software
19  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20  USA
21 */
22 #include "utap/builder.h"
23 #include "utap/system.h"
24 #include "utap/expression.h"
25 #include "utap/statement.h" // ExpressionVisitor for function call analysis
26 
27 #include <algorithm>
28 #include <stdexcept>
29 #include <cassert>
30 #include <cstring>
31 
32 using namespace UTAP;
33 using namespace Constants;
34 
35 using std::vector;
36 using std::set;
37 using std::min;
38 using std::max;
39 using std::pair;
40 using std::make_pair;
41 using std::map;
42 using std::ostream;
43 using Constants::kind_t;
45 
46 struct expression_t::expression_data
47 {
48  position_t position;
49  kind_t kind;
50  union
51  {
52  int32_t value;
53  int32_t index;
54  synchronisation_t sync;
55  double doubleValue;
56  };
58  type_t type;
59  std::vector<expression_t> sub;
60 // expression_data(){}
61  expression_data(position_t p, kind_t k, int32_t v):
62  position(p), kind(k), value(v) {}
63 };
64 
66 {
67  data = std::make_shared<expression_data>(pos, kind, 0);
68 }
69 
71 {
72  *this = e;
73 }
74 
76 {
77  data = e.data;
78  return *this;
79 }
80 
82 {
83  expression_t expr(data->kind, data->position);
84  expr.data->value = data->value;
85  expr.data->type = data->type;
86  expr.data->symbol = data->symbol;
87  expr.data->sub.reserve(data->sub.size());
88  expr.data->sub.assign(data->sub.begin(), data->sub.end());
89  return expr;
90 }
91 
93 {
94  expression_t expr(data->kind, data->position);
95  expr.data->value = data->value;
96  expr.data->type = data->type;
97  expr.data->symbol = data->symbol;
98  if (!data->sub.empty())
99  {
100  expr.data->sub.reserve(data->sub.size());
101  for (const auto& s: data->sub)
102  expr.data->sub.push_back(s.deeperClone());
103  }
104  return expr;
105 }
106 
108 {
109  expression_t expr(data->kind, data->position);
110  expr.data->value = data->value;
111  expr.data->type = data->type;
112  expr.data->symbol = (data->symbol == from) ? to : data->symbol;
113 
114  if (!data->sub.empty())
115  {
116  expr.data->sub.reserve(data->sub.size());
117  for (const auto& s: data->sub)
118  expr.data->sub.push_back(s.deeperClone(from, to));
119  }
120  return expr;
121 }
122 
124 {
125  expression_t expr(data->kind, data->position);
126  expr.data->value = data->value;
127  expr.data->type = data->type;
128  symbol_t uid;
129  if (data->symbol != symbol_t())
130  {
131  bool res = frame.resolve(data->symbol.getName(), uid);
132  if (!res && select != frame_t())
133  {
134  res = select.resolve(data->symbol.getName(), uid);
135  }
136  assert(res);
137  expr.data->symbol = uid;
138  }
139  else
140  {
141  expr.data->symbol = data->symbol;
142  }
143 
144  if (!data->sub.empty())
145  {
146  expr.data->sub.reserve(data->sub.size());
147  for (const auto& s: data->sub)
148  expr.data->sub.push_back(s.deeperClone(frame, select));
149  }
150  return expr;
151 }
152 
154 {
155  if (empty())
156  {
157  return *this;
158  }
159  else if (getKind() == IDENTIFIER && getSymbol() == symbol)
160  {
161  return expr;
162  }
163  else if (getSize() == 0)
164  {
165  return *this;
166  }
167  else
168  {
169  expression_t e = clone();
170  for (size_t i = 0; i < getSize(); i++)
171  {
172  e[i] = e[i].subst(symbol, expr);
173  }
174  return e;
175  }
176 }
177 
179 {
180 }
181 
183 {
184  assert(data);
185  return data->kind;
186 }
187 
189 {
190  assert(data);
191  return data->position;
192 }
193 
194 class FPStatementVisitor: public ExpressionVisitor
195 {
196  bool seenFP = false;
197 protected:
198  void visitExpression(expression_t expr) override {
199  seenFP |= expr.usesFP();
200  };
201 public:
202  bool operator()(Statement* s) {
203  seenFP = false;
204  s->accept(this);
205  return seenFP;
206  }
207 };
208 
209 bool checkForFP(Statement* s) { return FPStatementVisitor{}(s); }
210 
212 {
213  if (empty())
214  {
215  return false;
216  }
217  if (data->type.is(Constants::DOUBLE))
218  {
219  return true;
220  }
221  switch(data->kind)
222  {
223  case FABS_F:
224  case FMOD_F:
225  case FMA_F:
226  case FMAX_F:
227  case FMIN_F:
228  case FDIM_F:
229  case EXP_F:
230  case EXP2_F:
231  case EXPM1_F:
232  case LN_F:
233  case LOG_F:
234  case LOG10_F:
235  case LOG2_F:
236  case LOG1P_F:
237  case POW_F:
238  case SQRT_F:
239  case CBRT_F:
240  case HYPOT_F:
241  case SIN_F:
242  case COS_F:
243  case TAN_F:
244  case ASIN_F:
245  case ACOS_F:
246  case ATAN_F:
247  case ATAN2_F:
248  case SINH_F:
249  case COSH_F:
250  case TANH_F:
251  case ASINH_F:
252  case ACOSH_F:
253  case ATANH_F:
254  case ERF_F:
255  case ERFC_F:
256  case TGAMMA_F:
257  case LGAMMA_F:
258  case CEIL_F:
259  case FLOOR_F:
260  case TRUNC_F:
261  case ROUND_F:
262  case FINT_F:
263  case LDEXP_F:
264  case ILOGB_F:
265  case LOGB_F:
266  case NEXTAFTER_F:
267  case COPYSIGN_F:
268  case FPCLASSIFY_F:
269  case ISFINITE_F:
270  case ISINF_F:
271  case ISNAN_F:
272  case ISNORMAL_F:
273  case SIGNBIT_F:
274  case ISUNORDERED_F:
275  case RANDOM_F:
276  case RANDOM_ARCSINE_F:
277  case RANDOM_BETA_F:
278  case RANDOM_GAMMA_F:
279  case RANDOM_NORMAL_F:
280  case RANDOM_POISSON_F:
281  case RANDOM_TRI_F:
282  case RANDOM_WEIBULL_F:
283  return true;
284  case FUNCALL: {
285  auto& symbol = get(0).getSymbol();
286  if (symbol.getType().isFunction() && symbol.getData())
287  {
288  auto* fun = (function_t*)symbol.getData();
289  if (fun && fun->body && checkForFP(fun->body))
290  return true;
291  }
292  }
293  default: ;
294  }
295 
296  size_t n = getSize();
297  for(size_t i = 0; i < n; ++i)
298  {
299  if (get(i).usesFP())
300  {
301  return true;
302  }
303  }
304 
305  return false;
306 }
307 
309 {
310  if (empty())
311  {
312  return false;
313  }
314  if (getType().isClock())
315  {
316  return true;
317  }
318  size_t n = getSize();
319  for(size_t i = 0; i < n; ++i)
320  {
321  if (get(i).usesClock())
322  {
323  return true;
324  }
325  }
326  return false;
327 }
328 
330 {
331  if (empty())
332  {
333  return false;
334  }
335  else
336  {
337  switch (data->kind)
338  {
339  case SPAWN:
340  case NUMOF:
341  case EXIT:
342  case SUMDYNAMIC:
343  case EXISTSDYNAMIC:
344  case FORALLDYNAMIC:
345  return true;
346  default:
347  ;
348  }
349  }
350  return false;
351 }
352 
354 {
355  bool hasIt = false;
356  size_t n = getSize ();
357  if (n <=0)
358  {
359  return false;
360  }
361  else
362  {
363  for (size_t i = 0;i<n;++i)
364  {
365  if (get(i).isDynamic ())
366  {
367  return true;
368  }
369  else
370  {
371  hasIt |= get(i).hasDynamicSub ();
372  }
373  }
374  }
375 
376  return hasIt;
377 }
378 
379 size_t expression_t::getSize() const
380 {
381  if (empty())
382  {
383  return 0;
384  }
385 
386  switch (data->kind)
387  {
388  case MINUS:
389  case PLUS:
390  case MULT:
391  case DIV:
392  case MOD:
393  case BIT_AND:
394  case BIT_OR:
395  case BIT_XOR:
396  case BIT_LSHIFT:
397  case BIT_RSHIFT:
398  case AND:
399  case OR:
400  case XOR:
401  case LT:
402  case LE:
403  case EQ:
404  case NEQ:
405  case GE:
406  case GT:
407  case SIMULATION_LE:
408  case SIMULATION_GE:
409  case REFINEMENT_LE:
410  case REFINEMENT_GE:
411  case CONSISTENCY:
412  case TIOQUOTIENT:
413  case MIN:
414  case MAX:
415  case ARRAY:
416  case COMMA:
417  case ASSIGN:
418  case ASSPLUS:
419  case ASSMINUS:
420  case ASSDIV:
421  case ASSMOD:
422  case ASSMULT:
423  case ASSAND:
424  case ASSOR:
425  case ASSXOR:
426  case ASSLSHIFT:
427  case ASSRSHIFT:
428  case FORALL:
429  case EXISTS:
430  case SUM:
431  case RESTRICT:
432  case SUP_VAR:
433  case INF_VAR:
434  case FRACTION:
435  case FMOD_F:
436  case FMAX_F:
437  case FMIN_F:
438  case FDIM_F:
439  case POW_F:
440  case HYPOT_F:
441  case ATAN2_F:
442  case LDEXP_F:
443  case NEXTAFTER_F:
444  case COPYSIGN_F:
445  case RANDOM_ARCSINE_F:
446  case RANDOM_BETA_F:
447  case RANDOM_GAMMA_F:
448  case RANDOM_NORMAL_F:
449  case RANDOM_WEIBULL_F:
450  assert(data->sub.size() == 2);
451  return 2;
452 
453  case UNARY_MINUS:
454  case NOT:
455  case DOT:
456  case SYNC:
457  case PREINCREMENT:
458  case POSTINCREMENT:
459  case PREDECREMENT:
460  case POSTDECREMENT:
461  case RATE:
462  case SPECIFICATION:
463  case IMPLEMENTATION:
464  case ABS_F:
465  case FABS_F:
466  case EXP_F:
467  case EXP2_F:
468  case EXPM1_F:
469  case LN_F:
470  case LOG_F:
471  case LOG10_F:
472  case LOG2_F:
473  case LOG1P_F:
474  case SQRT_F:
475  case CBRT_F:
476  case SIN_F:
477  case COS_F:
478  case TAN_F:
479  case ASIN_F:
480  case ACOS_F:
481  case ATAN_F:
482  case SINH_F:
483  case COSH_F:
484  case TANH_F:
485  case ASINH_F:
486  case ACOSH_F:
487  case ATANH_F:
488  case ERF_F:
489  case ERFC_F:
490  case TGAMMA_F:
491  case LGAMMA_F:
492  case CEIL_F:
493  case FLOOR_F:
494  case TRUNC_F:
495  case ROUND_F:
496  case FINT_F:
497  case ILOGB_F:
498  case LOGB_F:
499  case FPCLASSIFY_F:
500  case ISFINITE_F:
501  case ISINF_F:
502  case ISNAN_F:
503  case ISNORMAL_F:
504  case SIGNBIT_F:
505  case ISUNORDERED_F:
506  case RANDOM_F:
507  case RANDOM_POISSON_F:
508  assert(data->sub.size() == 1);
509  return 1;
510 
511  case IDENTIFIER:
512  case CONSTANT:
513  case DEADLOCK:
514  assert(data->sub.size() == 0);
515  return 0;
516 
517  case INLINEIF:
518  case FMA_F:
519  case RANDOM_TRI_F:
520  assert(data->sub.size() == 3);
521  return 3;
522 
523  case FUNCALL:
524  case LIST:
525  case TIOCOMPOSITION:
526  case TIOCONJUNCTION:
527  case SIMULATE:
528  case SIMULATEREACH:
529  case SYNTAX_COMPOSITION:
530  case SPAWN:
531  return data->value;
532 
533  case EG:
534  case AG:
535  case EF:
536  case AF:
537  case EF_R_Piotr:
538  case AG_R_Piotr:
539  case CONTROL:
540  case EF_CONTROL:
541  case CONTROL_TOPT_DEF2:
542  case PMAX:
543  case SCENARIO:
544  assert(data->sub.size() == 1);
545  return 1;
546 
547  case LEADSTO:
548  case SCENARIO2:
549  case A_UNTIL:
550  case A_WEAKUNTIL:
551  case A_BUCHI:
552  case PO_CONTROL:
553  case CONTROL_TOPT_DEF1:
554  assert(data->sub.size() == 2);
555  return 2;
556 
557  case CONTROL_TOPT:
558  case SMC_CONTROL:
559  assert(data->sub.size() == 3);
560  return 3;
561  case PROBABOX:
562  case PROBADIAMOND:
563  case PROBAMINBOX:
564  case PROBAMINDIAMOND:
565  assert(data->sub.size() == 5);
566  return 5;
567 
568  case PROBAEXP:
569  assert(data->sub.size() == 5);
570  return 5;
571 
572  case PROBACMP:
573  assert(data->sub.size() == 8);
574  return 8;
575  case MITLFORMULA:
576  case MITLATOM:
577  case MITLNEXT:
578  assert(data->sub.size() == 1);
579  return 1;
580  case MITLDISJ:
581  case MITLCONJ:
582  assert(data->sub.size() == 2);
583  return 2;
584  case MITLUNTIL:
585  case MITLRELEASE:
586  assert(data->sub.size() == 4);
587  return 4;
588  case EXIT:
589  assert(data->sub.size() == 0);
590  return 0;
591  case NUMOF:
592  assert(data->sub.size() == 1);
593  return 1;
594  case EXISTSDYNAMIC:
595  case FORALLDYNAMIC:
596  case SUMDYNAMIC:
597  case MITLEXISTS:
598  case MITLFORALL:
599  case FOREACHDYNAMIC:
600  assert(data->sub.size() == 3);
601  return 3;
602  case DYNAMICEVAL:
603  assert(data->sub.size() == 2);
604  return 2;
605  default:
606  assert(0);
607  return 0;
608  }
609 }
610 
612 {
613  assert(data);
614  return data->type;
615 }
616 
618 {
619  assert(data);
620  data->type = type;
621 }
622 
623 int32_t expression_t::getValue() const
624 {
625  assert(data && data->kind == CONSTANT && data->type.isIntegral());
626  return data->type.isInteger() ? data->value : (data->value ? 1 : 0);
627 }
628 
630 {
631  assert(data && data->kind == CONSTANT && data->type.is(Constants::DOUBLE));
632  return data->doubleValue;
633 }
634 
635 int32_t expression_t::getIndex() const
636 {
637  assert(data && data->kind == DOT);
638  return data->index;
639 }
640 
642 {
643  assert(data && data->kind == SYNC);
644  return data->sync;
645 }
646 
648 {
649  assert(data && 0 <= i && i < getSize());
650  return data->sub[i];
651 }
652 
653 const expression_t expression_t::operator[](uint32_t i) const
654 {
655  assert(data && 0 <= i && i < getSize());
656  return data->sub[i];
657 }
658 
660 {
661  assert(data && 0 <= i && i < getSize());
662  return data->sub[i];
663 }
664 
665 const expression_t &expression_t::get(uint32_t i) const
666 {
667  assert(data && 0 <= i && i < getSize());
668  return data->sub[i];
669 }
670 
672 {
673  return data == NULL;
674 }
675 
677 {
678  return data == NULL || (getType().isIntegral() && data->kind == CONSTANT && getValue() == 1);
679 }
680 
681 
685 bool expression_t::equal(const expression_t &e) const
686 {
687  if (data == e.data)
688  {
689  return true;
690  }
691 
692  if (getSize() != e.getSize()
693  || data->kind != e.data->kind
694  || data->value != e.data->value
695  || data->symbol != e.data->symbol)
696  {
697  return false;
698  }
699 
700  for (uint32_t i = 0; i < getSize(); i++)
701  {
702  if (!data->sub[i].equal(e[i]))
703  {
704  return false;
705  }
706  }
707 
708  return true;
709 }
710 
719 {
720  return ((const expression_t*)this)->getSymbol();
721 }
722 
724 {
725  assert(data);
726 
727  switch (getKind())
728  {
729  case IDENTIFIER:
730  return data->symbol;
731 
732  case DOT:
733  return get(0).getSymbol();
734 
735  case ARRAY:
736  return get(0).getSymbol();
737 
738  case PREINCREMENT:
739  case PREDECREMENT:
740  return get(0).getSymbol();
741 
742  case INLINEIF:
743  return get(1).getSymbol();
744 
745  case COMMA:
746  return get(1).getSymbol();
747 
748  case ASSIGN:
749  case ASSPLUS:
750  case ASSMINUS:
751  case ASSDIV:
752  case ASSMOD:
753  case ASSMULT:
754  case ASSAND:
755  case ASSOR:
756  case ASSXOR:
757  case ASSLSHIFT:
758  case ASSRSHIFT:
759  return get(0).getSymbol();
760 
761  case SYNC:
762  return get(0).getSymbol();
763 
764  case FUNCALL:
765  return get(0).getSymbol();
766 
767  case SCENARIO:
768  return get(0).getSymbol();
769 
770  default:
771  return symbol_t();
772  }
773 }
774 
775 void expression_t::getSymbols(std::set<symbol_t> &symbols) const
776 {
777  if (empty())
778  {
779  return;
780  }
781 
782  switch (getKind())
783  {
784  case IDENTIFIER:
785  symbols.insert(data->symbol);
786  break;
787 
788  case DOT:
789  get(0).getSymbols(symbols);
790  break;
791 
792  case ARRAY:
793  get(0).getSymbols(symbols);
794  break;
795 
796  case PREINCREMENT:
797  case PREDECREMENT:
798  get(0).getSymbols(symbols);
799  break;
800 
801  case INLINEIF:
802  get(1).getSymbols(symbols);
803  get(2).getSymbols(symbols);
804  break;
805 
806  case COMMA:
807  get(1).getSymbols(symbols);
808  break;
809 
810  case ASSIGN:
811  case ASSPLUS:
812  case ASSMINUS:
813  case ASSDIV:
814  case ASSMOD:
815  case ASSMULT:
816  case ASSAND:
817  case ASSOR:
818  case ASSXOR:
819  case ASSLSHIFT:
820  case ASSRSHIFT:
821  get(0).getSymbols(symbols);
822  break;
823 
824  case SYNC:
825  get(0).getSymbols(symbols);
826  break;
827 
828  default:
829  // Do nothing
830  break;
831  }
832 }
833 
836 bool expression_t::isReferenceTo(const std::set<symbol_t> &symbols) const
837 {
838  std::set<symbol_t> s;
839  getSymbols(s);
840  return find_first_of(symbols.begin(), symbols.end(), s.begin(), s.end())
841  != symbols.end();
842 }
843 
844 bool expression_t::changesVariable(const std::set<symbol_t> &symbols) const
845 {
846  std::set<symbol_t> changes;
847  collectPossibleWrites(changes);
848  return find_first_of(symbols.begin(), symbols.end(),
849  changes.begin(), changes.end()) != symbols.end();
850 }
851 
853 {
854  std::set<symbol_t> changes;
855  collectPossibleWrites(changes);
856  return !changes.empty();
857 }
858 
859 bool expression_t::dependsOn(const std::set<symbol_t> &symbols) const
860 {
861  std::set<symbol_t> dependencies;
862  collectPossibleReads(dependencies);
863  return find_first_of(
864  symbols.begin(), symbols.end(),
865  dependencies.begin(), dependencies.end()) != symbols.end();
866 }
867 
868 int expression_t::getPrecedence() const
869 {
870  return getPrecedence(data->kind);
871 }
872 
873 int expression_t::getPrecedence(kind_t kind)
874 {
875  switch (kind)
876  {
877  case PLUS:
878  case MINUS:
879  return 70;
880 
881  case MULT:
882  case DIV:
883  case MOD:
884  return 80;
885 
886  case BIT_AND:
887  return 37;
888 
889  case BIT_OR:
890  return 30;
891 
892  case BIT_XOR:
893  return 35;
894 
895  case BIT_LSHIFT:
896  case BIT_RSHIFT:
897  return 60;
898 
899  case AND:
900  return 25;
901  case OR:
902  return 22;
903  case XOR:
904  return 20;
905 
906  case EQ:
907  case NEQ:
908  return 40;
909 
910  case MIN:
911  case MAX:
912  return 55;
913 
914  case RESTRICT:
915  return 60;
916 
917  case LT:
918  case LE:
919  case GE:
920  case GT:
921  case SIMULATION_LE:
922  case SIMULATION_GE:
923  case REFINEMENT_LE:
924  case REFINEMENT_GE:
925  case SIMULATE:
926  return 50;
927 
928  case IDENTIFIER:
929  case CONSTANT:
930  case DEADLOCK:
931  case FUNCALL:
932  return 110;
933 
934  case DOT:
935  case ARRAY:
936  case RATE:
937  return 100;
938 
939  case UNARY_MINUS:
940  case NOT:
941  return 90;
942 
943  case FRACTION:
944  return 14;
945  case INLINEIF:
946  return 15;
947 
948  case ASSIGN:
949  case ASSPLUS:
950  case ASSMINUS:
951  case ASSDIV:
952  case ASSMOD:
953  case ASSMULT:
954  case ASSAND:
955  case ASSOR:
956  case ASSXOR:
957  case ASSLSHIFT:
958  case ASSRSHIFT:
959  return 10;
960 
961  case FORALL:
962  case EXISTS:
963  case SUM:
964  return 8;
965 
966  case IMPLEMENTATION:
967  case SPECIFICATION:
968  case CONSISTENCY:
969  case TIOQUOTIENT:
970  case TIOCONJUNCTION:
971  case TIOCOMPOSITION:
972  case SYNTAX_COMPOSITION:
973  case A_UNTIL:
974  case A_WEAKUNTIL:
975  case A_BUCHI:
976  return 7;
977 
978  case EF:
979  case EG:
980  case AF:
981  case AG:
982  case EF_R_Piotr:
983  case AG_R_Piotr:
984  return 6;
985 
986  case LEADSTO:
987  case SCENARIO:
988  case SCENARIO2:
989  return 5;
990 
991  case COMMA:
992  return 4;
993 
994  case PROBAMINBOX:
995  case PROBAMINDIAMOND:
996  case PROBABOX:
997  case PROBADIAMOND:
998  case PROBAEXP:
999  case PO_CONTROL:
1000  case CONTROL:
1001  case SMC_CONTROL:
1002  case EF_CONTROL:
1003  case CONTROL_TOPT:
1004  case CONTROL_TOPT_DEF1:
1005  case CONTROL_TOPT_DEF2:
1006  case SUP_VAR:
1007  case INF_VAR:
1008  return 3;
1009 
1010  case SYNC:
1011  return 0;
1012 
1013  case PREDECREMENT:
1014  case POSTDECREMENT:
1015  case PREINCREMENT:
1016  case POSTINCREMENT:
1017  case ABS_F:
1018  case FABS_F:
1019  case FMOD_F:
1020  case FMA_F:
1021  case FMAX_F:
1022  case FMIN_F:
1023  case FDIM_F:
1024  case EXP_F:
1025  case EXP2_F:
1026  case EXPM1_F:
1027  case LN_F:
1028  case LOG_F:
1029  case LOG10_F:
1030  case LOG2_F:
1031  case LOG1P_F:
1032  case POW_F:
1033  case SQRT_F:
1034  case CBRT_F:
1035  case HYPOT_F:
1036  case SIN_F:
1037  case COS_F:
1038  case TAN_F:
1039  case ASIN_F:
1040  case ACOS_F:
1041  case ATAN_F:
1042  case ATAN2_F:
1043  case SINH_F:
1044  case COSH_F:
1045  case TANH_F:
1046  case ASINH_F:
1047  case ACOSH_F:
1048  case ATANH_F:
1049  case ERF_F:
1050  case ERFC_F:
1051  case TGAMMA_F:
1052  case LGAMMA_F:
1053  case CEIL_F:
1054  case FLOOR_F:
1055  case TRUNC_F:
1056  case ROUND_F:
1057  case FINT_F:
1058  case LDEXP_F:
1059  case ILOGB_F:
1060  case LOGB_F:
1061  case NEXTAFTER_F:
1062  case COPYSIGN_F:
1063  case FPCLASSIFY_F:
1064  case ISFINITE_F:
1065  case ISINF_F:
1066  case ISNAN_F:
1067  case ISNORMAL_F:
1068  case SIGNBIT_F:
1069  case ISUNORDERED_F:
1070  case RANDOM_F:
1071  case RANDOM_ARCSINE_F:
1072  case RANDOM_BETA_F:
1073  case RANDOM_GAMMA_F:
1074  case RANDOM_NORMAL_F:
1075  case RANDOM_POISSON_F:
1076  case RANDOM_WEIBULL_F:
1077  case RANDOM_TRI_F:
1078  return 100;
1079 
1080  case MITLFORMULA:
1081  case MITLUNTIL:
1082  case MITLRELEASE:
1083  case MITLDISJ:
1084  case MITLCONJ:
1085  case MITLATOM:
1086  case MITLNEXT:
1087  case LIST:
1088  case SPAWN:
1089  case EXIT:
1090  case NUMOF:
1091  case FORALLDYNAMIC:
1092  case EXISTSDYNAMIC:
1093  case FOREACHDYNAMIC:
1094  case SUMDYNAMIC:
1095  case PROCESSVAR:
1096  case DYNAMICEVAL:
1097  return -1; // TODO
1098 
1099  default:
1100  throw std::runtime_error("Strange expression");
1101  }
1102  assert(0);
1103  return 0;
1104 }
1105 
1106 static void ensure(char *&str, char *&end, int &size, int len)
1107 {
1108  while (size <= len)
1109  {
1110  size *= 2;
1111  }
1112 
1113  char *nstr = new char[size];
1114  strncpy(nstr, str, end - str);
1115  end = nstr + (end - str);
1116  *end = 0;
1117  delete[] str;
1118  str = nstr;
1119 }
1120 
1121 static void append(char *&str, char *&end, int &size, const char *s)
1122 {
1123  while (end < str + size && *s)
1124  {
1125  *(end++) = *(s++);
1126  }
1127 
1128  if (end == str + size)
1129  {
1130  ensure(str, end, size, 2 * size);
1131  append(str, end, size, s);
1132  }
1133  else
1134  {
1135  *end = 0;
1136  }
1137 }
1138 
1139 static void append(char *&str, char *&end, int &size, char c)
1140 {
1141  if (size - (end - str) < 2)
1142  {
1143  ensure(str, end, size, size + 2);
1144  }
1145  *end = c;
1146  ++end;
1147  *end = 0;
1148 }
1149 
1150 void expression_t::appendBoundType(char *&str, char*&end, int &size, expression_t e) const
1151 {
1152  if (e.getKind() == CONSTANT)
1153  {
1154  assert(e.getType().is(Constants::INT)); // Encoding used here.
1155 
1156  if (e.getValue() == 0)
1157  {
1158  append(str, end, size, "#");
1159  }
1160  }
1161  else
1162  {
1163  e.toString(false, str, end, size);
1164  }
1165  append(str, end, size, "<=");
1166 }
1167 
1168 static
1169 const char* getBuiltinFunName(kind_t kind)
1170 {
1171  // the order must match declarations in include/utap/common.h
1172  static const char* funNames[] = {
1173  "abs", "fabs", "fmod", "fma", "fmax", "fmin", "fdim",
1174  "exp", "exp2", "expm1", "ln", "log", "log10", "log2", "log1p",
1175  "pow", "sqrt", "cbrt", "hypot",
1176  "sin", "cos", "tan", "asin", "acos", "atan", "atan2",
1177  "sinh", "cosh", "tanh", "asinh", "acosh", "atanh",
1178  "erf", "erfc", "tgamma", "lgamma",
1179  "ceil", "floor", "trunc", "round", "fint",
1180  "ldexp", "ilogb", "logb", "nextafter", "copysign",
1181  "fpclassify", "isfinite", "isinf", "isnan", "isnormal", "signbit",
1182  "isunordered", "random", "random_arcsine", "random_beta",
1183  "random_gamma", "random_normal", "random_poisson",
1184  "random_weibull", "random_tri"
1185  };
1186  static_assert(RANDOM_TRI_F-ABS_F+1 == sizeof(funNames)/sizeof(funNames[0]),
1187  "Builtin function name list is wrong");
1188  assert(ABS_F <= kind && kind <= RANDOM_TRI_F);
1189  return funNames[kind-ABS_F];
1190 }
1191 
1192 void expression_t::toString(bool old, char *&str, char *&end, int &size) const
1193 {
1194  char s[64];
1195  int precedence = getPrecedence();
1196  bool flag = false;
1197  int nb;
1198 
1199  switch (data->kind)
1200  {
1201  case PROBAMINBOX:
1202  flag = true;
1203  case PROBAMINDIAMOND:
1204  append(str,end, size, "Pr[");
1205  appendBoundType(str, end, size, get(1));
1206  get(2).toString(old, str, end, size);
1207  if (get(0).getValue()>0)
1208  get(0).toString(old, str, end, size);
1209  append(str,end, size, flag ? "]([] " : "](<> ");
1210  get(3).toString(old, str, end, size);
1211  append(str,end, size, ") >= ");
1212  snprintf(s,sizeof(s),"%f",get(4).getDoubleValue());
1213  append(str,end, size, s);
1214  break;
1215 
1216  case PROBABOX:
1217  flag = true;
1218  case PROBADIAMOND:
1219  append(str, end, size, "Pr[");
1220  appendBoundType(str, end, size, get(1));
1221  get(2).toString(old, str, end, size);
1222  if (get(0).getValue()>0)
1223  get(0).toString(old, str, end, size);
1224  append(str, end, size, flag ? "]([] " : "](<> ");
1225  get(3).toString(old, str, end, size);
1226  append(str, end, size, ") ?");
1227  break;
1228 
1229  case PROBAEXP:
1230  append(str, end, size, "E[");
1231  appendBoundType(str, end, size, get(1));
1232  get(2).toString(old, str, end, size);
1233  append(str, end, size, "; ");
1234  get(0).toString(old, str, end, size);
1235  append(str, end, size, "] (");
1236  append(str, end, size, get(3).getValue() ? "max: " : "min: ");
1237  get(4).toString(old, str, end, size);
1238  append(str, end, size, ")");
1239  break;
1240 
1241  case SIMULATE:
1242  append(str, end, size, "simulate[");
1243  get(0).toString(old, str, end, size);
1244  append(str, end, size, "x ");
1245  appendBoundType(str, end, size, get(1));
1246  get(2).toString(old, str, end, size);
1247  append(str, end, size, "]{");
1248  nb = getValue() - 3;
1249  for(int i = 0; i < nb; ++i)
1250  {
1251  if (i > 0)
1252  append(str, end, size, ", ");
1253  get(3+i).toString(old, str, end, size);
1254  }
1255  append(str, end, size, "}");
1256  break;
1257 
1258  case TIOCONJUNCTION:
1259  flag = true;
1260  case TIOCOMPOSITION:
1261  append(str, end, size, "(");
1262  get(0).toString(old, str, end, size);
1263  for (uint32_t i = 1; i < getSize(); i++)
1264  {
1265  append(str, end, size, flag ? " && " : " || ");
1266  get(i).toString(old, str, end, size);
1267  }
1268  append(str, end, size, ")");
1269  break;
1270 
1271  case SYNTAX_COMPOSITION:
1272  append(str, end, size, "(");
1273  get(0).toString(old, str, end, size);
1274  for (uint32_t i = 1; i < getSize(); i++)
1275  {
1276  append(str, end, size, " + ");
1277  get(i).toString(old, str, end, size);
1278  }
1279  append(str, end, size, ")");
1280  break;
1281 
1282  case IMPLEMENTATION:
1283  append(str, end, size, "implementation: ");
1284  get(0).toString(old, str, end, size);
1285  break;
1286 
1287  case SPECIFICATION:
1288  append(str, end, size, "specification: ");
1289  get(0).toString(old, str, end, size);
1290  break;
1291 
1292  case CONSISTENCY:
1293  append(str, end, size, "consistency: ");
1294  get(0).toString(old, str, end, size);
1295  if (!(get(1).getKind() == AG &&
1296  get(1).get(0).getKind() == CONSTANT &&
1297  get(1).get(0).getValue() == 1))
1298  {
1299  append(str, end, size, " : ");
1300  get(1).toString(old, str, end, size);
1301  }
1302  break;
1303 
1304  case SIMULATION_GE:
1305  flag = true;
1306  case REFINEMENT_GE:
1307  append(str, end, size, flag ? "simulation: {" : "refinement: {");
1308  get(0).toString(old, str, end, size);
1309  append(str, end, size, flag ? "} >= " : " >= ");
1310  get(1).toString(old, str, end, size);
1311  break;
1312 
1313  case SIMULATION_LE:
1314  flag = true;
1315  case REFINEMENT_LE:
1316  append(str, end, size, flag ? "simulation: " : "refinement: ");
1317  get(0).toString(old, str, end, size);
1318  append(str, end, size, flag ? " <= {" : " <= ");
1319  get(1).toString(old, str, end, size);
1320  if (flag) append(str, end, size, "}");
1321  break;
1322 
1323  case RESTRICT:
1324  append(str, end, size, "{");
1325  get(0).toString(old, str, end, size);
1326  append(str, end, size, "}\{");
1327  get(1).toString(old, str, end, size);
1328  append(str, end, size, "}");
1329  break;
1330 
1331  case PLUS:
1332  case MINUS:
1333  case MULT:
1334  case DIV:
1335  case MOD:
1336  case BIT_AND:
1337  case BIT_OR:
1338  case BIT_XOR:
1339  case BIT_LSHIFT:
1340  case BIT_RSHIFT:
1341  case AND:
1342  case OR:
1343  case LT:
1344  case LE:
1345  case EQ:
1346  case NEQ:
1347  case GE:
1348  case GT:
1349  case ASSIGN:
1350  case ASSPLUS:
1351  case ASSMINUS:
1352  case ASSDIV:
1353  case ASSMOD:
1354  case ASSMULT:
1355  case ASSAND:
1356  case ASSOR:
1357  case ASSXOR:
1358  case ASSLSHIFT:
1359  case ASSRSHIFT:
1360  case MIN:
1361  case MAX:
1362  case TIOQUOTIENT:
1363  case FRACTION:
1364 
1365  if (precedence > get(0).getPrecedence())
1366  {
1367  append(str, end, size, '(');
1368  }
1369  get(0).toString(old, str, end, size);
1370  if (precedence > get(0).getPrecedence())
1371  {
1372  append(str, end, size, ')');
1373  }
1374 
1375  switch (data->kind)
1376  {
1377  case FRACTION:
1378  append(str, end, size, " : ");
1379  break;
1380  case PLUS:
1381  append(str, end, size, " + ");
1382  break;
1383  case MINUS:
1384  append(str, end, size, " - ");
1385  break;
1386  case MULT:
1387  append(str, end, size, " * ");
1388  break;
1389  case DIV:
1390  append(str, end, size, " / ");
1391  break;
1392  case MOD:
1393  append(str, end, size, " % ");
1394  break;
1395  case BIT_AND:
1396  append(str, end, size, " & ");
1397  break;
1398  case BIT_OR:
1399  append(str, end, size, " | ");
1400  break;
1401  case BIT_XOR:
1402  append(str, end, size, " ^ ");
1403  break;
1404  case BIT_LSHIFT:
1405  append(str, end, size, " << ");
1406  break;
1407  case BIT_RSHIFT:
1408  append(str, end, size, " >> ");
1409  break;
1410  case AND:
1411  append(str, end, size, " && ");
1412  break;
1413  case OR:
1414  append(str, end, size, " || ");
1415  break;
1416  case LT:
1417  append(str, end, size, " < ");
1418  break;
1419  case LE:
1420  append(str, end, size, " <= ");
1421  break;
1422  case EQ:
1423  append(str, end, size, " == ");
1424  break;
1425  case NEQ:
1426  append(str, end, size, " != ");
1427  break;
1428  case GE:
1429  append(str, end, size, " >= ");
1430  break;
1431  case GT:
1432  append(str, end, size, " > ");
1433  break;
1434  case ASSIGN:
1435  if (old)
1436  {
1437  append(str, end, size, " := ");
1438  }
1439  else
1440  {
1441  append(str, end, size, " = ");
1442  }
1443  break;
1444  case ASSPLUS:
1445  append(str, end, size, " += ");
1446  break;
1447  case ASSMINUS:
1448  append(str, end, size, " -= ");
1449  break;
1450  case ASSDIV:
1451  append(str, end, size, " /= ");
1452  break;
1453  case ASSMOD:
1454  append(str, end, size, " %= ");
1455  break;
1456  case ASSMULT:
1457  append(str, end, size, " *= ");
1458  break;
1459  case ASSAND:
1460  append(str, end, size, " &= ");
1461  break;
1462  case ASSOR:
1463  append(str, end, size, " |= ");
1464  break;
1465  case ASSXOR:
1466  append(str, end, size, " ^= ");
1467  break;
1468  case ASSLSHIFT:
1469  append(str, end, size, " <<= ");
1470  break;
1471  case ASSRSHIFT:
1472  append(str, end, size, " >>= ");
1473  break;
1474  case MIN:
1475  append(str, end, size, " <? ");
1476  break;
1477  case MAX:
1478  append(str, end, size, " >? ");
1479  break;
1480  case TIOQUOTIENT:
1481  append(str, end, size, " \\ ");
1482  break;
1483  default:
1484  assert(0);
1485  }
1486 
1487  if (precedence >= get(1).getPrecedence())
1488  {
1489  append(str, end, size, '(');
1490  }
1491  get(1).toString(old, str, end, size);
1492  if (precedence >= get(1).getPrecedence())
1493  {
1494  append(str, end, size, ')');
1495  }
1496  break;
1497 
1498  case IDENTIFIER:
1499  append(str, end, size, data->symbol.getName().c_str());
1500  break;
1501 
1502  case CONSTANT:
1503  if (getType().is(Constants::DOUBLE))
1504  {
1505  snprintf(s,sizeof(s),"%f",getDoubleValue());
1506  }
1507  else if (getType().is(Constants::INT))
1508  {
1509  snprintf(s,sizeof(s), "%d", data->value);
1510  }
1511  else
1512  {
1513  assert(getType().is(Constants::BOOL));
1514  snprintf(s, sizeof(s), "%s", data->value ? "true" : "false");
1515  }
1516  append(str,end,size,s);
1517  break;
1518 
1519  case ARRAY:
1520  if (precedence > get(0).getPrecedence())
1521  {
1522  append(str, end, size, '(');
1523  get(0).toString(old, str, end, size);
1524  append(str, end, size, ')');
1525  }
1526  else
1527  {
1528  get(0).toString(old, str, end, size);
1529  }
1530  append(str, end, size, '[');
1531  get(1).toString(old, str, end, size);
1532  append(str, end, size, ']');
1533  break;
1534 
1535  case UNARY_MINUS:
1536  append(str, end, size, '-');
1537  if (precedence > get(0).getPrecedence())
1538  {
1539  append(str, end, size, '(');
1540  get(0).toString(old, str, end, size);
1541  append(str, end, size, ')');
1542  }
1543  else
1544  {
1545  get(0).toString(old, str, end, size);
1546  }
1547  break;
1548 
1549  case POSTDECREMENT:
1550  case POSTINCREMENT:
1551  if (precedence > get(0).getPrecedence())
1552  {
1553  append(str, end, size, '(');
1554  get(0).toString(old, str, end, size);
1555  append(str, end, size, ')');
1556  }
1557  else
1558  {
1559  get(0).toString(old, str, end, size);
1560  }
1561  append(str, end, size, getKind() == POSTDECREMENT ? "--" : "++");
1562  break;
1563 
1564  case ABS_F:
1565  case FABS_F:
1566  case EXP_F:
1567  case EXP2_F:
1568  case EXPM1_F:
1569  case LN_F:
1570  case LOG_F:
1571  case LOG10_F:
1572  case LOG2_F:
1573  case LOG1P_F:
1574  case SQRT_F:
1575  case CBRT_F:
1576  case SIN_F:
1577  case COS_F:
1578  case TAN_F:
1579  case ASIN_F:
1580  case ACOS_F:
1581  case ATAN_F:
1582  case SINH_F:
1583  case COSH_F:
1584  case TANH_F:
1585  case ASINH_F:
1586  case ACOSH_F:
1587  case ATANH_F:
1588  case ERF_F:
1589  case ERFC_F:
1590  case TGAMMA_F:
1591  case LGAMMA_F:
1592  case CEIL_F:
1593  case FLOOR_F:
1594  case TRUNC_F:
1595  case ROUND_F:
1596  case FINT_F:
1597  case ILOGB_F:
1598  case LOGB_F:
1599  case FPCLASSIFY_F:
1600  case ISFINITE_F:
1601  case ISINF_F:
1602  case ISNAN_F:
1603  case ISNORMAL_F:
1604  case SIGNBIT_F:
1605  case ISUNORDERED_F:
1606  case RANDOM_F:
1607  case RANDOM_POISSON_F:
1608  append(str, end, size, getBuiltinFunName(data->kind));
1609  append(str, end, size, "(");
1610  get(0).toString(old, str, end, size);
1611  append(str, end, size, ')');
1612  break;
1613 
1614  case FMOD_F:
1615  case FMAX_F:
1616  case FMIN_F:
1617  case FDIM_F:
1618  case POW_F:
1619  case HYPOT_F:
1620  case ATAN2_F:
1621  case LDEXP_F:
1622  case NEXTAFTER_F:
1623  case COPYSIGN_F:
1624  case RANDOM_ARCSINE_F:
1625  case RANDOM_BETA_F:
1626  case RANDOM_GAMMA_F:
1627  case RANDOM_NORMAL_F:
1628  case RANDOM_WEIBULL_F:
1629  append(str, end, size, getBuiltinFunName(data->kind));
1630  append(str, end, size, "(");
1631  get(0).toString(old, str, end, size);
1632  append(str, end, size, ',');
1633  get(1).toString(old, str, end, size);
1634  append(str, end, size, ')');
1635  break;
1636 
1637  case FMA_F:
1638  case RANDOM_TRI_F:
1639  append(str, end, size, getBuiltinFunName(data->kind));
1640  append(str, end, size, "(");
1641  get(0).toString(old, str, end, size);
1642  append(str, end, size, ',');
1643  get(1).toString(old, str, end, size);
1644  append(str, end, size, ',');
1645  get(2).toString(old, str, end, size);
1646  append(str, end, size, ')');
1647  break;
1648 
1649  case XOR:
1650  append(str, end, size, '(');
1651  get(0).toString(old, str, end, size);
1652  append(str, end, size, ") xor (");
1653  get(1).toString(old, str, end, size);
1654  append(str, end, size, ')');
1655  break;
1656 
1657  case PREDECREMENT:
1658  case PREINCREMENT:
1659  append(str, end, size, getKind() == PREDECREMENT ? "--" : "++");
1660  if (precedence > get(0).getPrecedence())
1661  {
1662  append(str, end, size, '(');
1663  get(0).toString(old, str, end, size);
1664  append(str, end, size, ')');
1665  }
1666  else
1667  {
1668  get(0).toString(old, str, end, size);
1669  }
1670  break;
1671 
1672  case NOT:
1673  append(str, end, size, '!');
1674  if (precedence > get(0).getPrecedence())
1675  {
1676  append(str, end, size, '(');
1677  get(0).toString(old, str, end, size);
1678  append(str, end, size, ')');
1679  }
1680  else
1681  {
1682  get(0).toString(old, str, end, size);
1683  }
1684  break;
1685 
1686  case DOT:
1687  {
1688  type_t type = get(0).getType();
1689  if (type.isProcess() || type.isRecord())
1690  {
1691  if (precedence > get(0).getPrecedence())
1692  {
1693  append(str, end, size, '(');
1694  get(0).toString(old, str, end, size);
1695  append(str, end, size, ')');
1696  }
1697  else
1698  {
1699  get(0).toString(old, str, end, size);
1700  }
1701  append(str, end, size, '.');
1702  append(str, end, size, type.getRecordLabel(data->value).c_str());
1703  }
1704  else
1705  {
1706  assert(0);
1707  }
1708  break;
1709  }
1710 
1711  case INLINEIF:
1712  if (precedence >= get(0).getPrecedence())
1713  {
1714  append(str, end, size, '(');
1715  get(0).toString(old, str, end, size);
1716  append(str, end, size, ')');
1717  }
1718  else
1719  {
1720  get(0).toString(old, str, end, size);
1721  }
1722 
1723  append(str, end, size, " ? ");
1724 
1725  if (precedence >= get(1).getPrecedence())
1726  {
1727  append(str, end, size, '(');
1728  get(1).toString(old, str, end, size);
1729  append(str, end, size, ')');
1730  }
1731  else
1732  {
1733  get(1).toString(old, str, end, size);
1734  }
1735 
1736  append(str, end, size, " : ");
1737 
1738  if (precedence >= get(2).getPrecedence())
1739  {
1740  append(str, end, size, '(');
1741  get(2).toString(old, str, end, size);
1742  append(str, end, size, ')');
1743  }
1744  else
1745  {
1746  get(2).toString(old, str, end, size);
1747  }
1748 
1749  break;
1750 
1751  case COMMA:
1752  get(0).toString(old, str, end, size);
1753  append(str, end, size, ", ");
1754  get(1).toString(old, str, end, size);
1755  break;
1756 
1757  case SYNC:
1758  get(0).toString(old, str, end, size);
1759  switch (data->sync)
1760  {
1761  case SYNC_QUE:
1762  append(str, end, size, '?');
1763  break;
1764  case SYNC_BANG:
1765  append(str, end, size, '!');
1766  break;
1767  case SYNC_CSP:
1768  // no append
1769  break;
1770  }
1771  break;
1772 
1773  case DEADLOCK:
1774  append(str, end, size, "deadlock");
1775  break;
1776 
1777  case LIST:
1778  get(0).toString(old, str, end, size);
1779  for (uint32_t i = 1; i < getSize(); i++)
1780  {
1781  append(str, end, size, ", ");
1782  get(i).toString(old, str, end, size);
1783  }
1784  break;
1785 
1786  case FUNCALL:
1787  get(0).toString(old, str, end, size);
1788  append(str, end, size, '(');
1789  if (getSize() > 1)
1790  {
1791  get(1).toString(old, str, end, size);
1792  for (uint32_t i = 2; i < getSize(); i++)
1793  {
1794  append(str, end, size, ", ");
1795  get(i).toString(old, str, end, size);
1796  }
1797  }
1798  append(str, end, size, ')');
1799  break;
1800 
1801  case RATE:
1802  get(0).toString(old, str, end, size);
1803  append(str, end, size, "'");
1804  break;
1805 
1806  case EF:
1807  append(str, end, size, "E<> ");
1808  get(0).toString(old, str, end, size);
1809  break;
1810 
1811  case EF_R_Piotr:
1812  append(str, end, size, "E<>* ");
1813  get(0).toString(old, str, end, size);
1814  break;
1815 
1816  case EG:
1817  append(str, end, size, "E[] ");
1818  get(0).toString(old, str, end, size);
1819  break;
1820 
1821  case AF:
1822  append(str, end, size, "A<> ");
1823  get(0).toString(old, str, end, size);
1824  break;
1825 
1826  case AG:
1827  append(str, end, size, "A[] ");
1828  get(0).toString(old, str, end, size);
1829  break;
1830 
1831  case AG_R_Piotr:
1832  append(str, end, size, "A[]* ");
1833  get(0).toString(old, str, end, size);
1834  break;
1835 
1836  case LEADSTO:
1837  get(0).toString(old, str, end, size);
1838  append(str, end, size, " --> ");
1839  get(1).toString(old, str, end, size);
1840  break;
1841 
1842  case A_UNTIL:
1843  append(str, end, size, "A[");
1844  get(0).toString(old, str, end, size);
1845  append(str, end, size, " U ");
1846  get(1).toString(old, str, end, size);
1847  append(str, end, size, "] ");
1848  break;
1849 
1850  case A_WEAKUNTIL:
1851  append(str, end, size, "A[");
1852  get(0).toString(old, str, end, size);
1853  append(str, end, size, " W ");
1854  get(1).toString(old, str, end, size);
1855  append(str, end, size, "] ");
1856  break;
1857 
1858  case A_BUCHI:
1859  append(str, end, size, "A[] ((");
1860  get(0).toString(old, str, end, size);
1861  append(str, end, size, ") and A<> ");
1862  get(1).toString(old, str, end, size);
1863  append(str, end, size, ") ");
1864  break;
1865 
1866  case FORALL:
1867  append(str, end, size, "forall (");
1868  append(str, end, size, get(0).getSymbol().getName().c_str());
1869  append(str, end, size, ":");
1870  append(str, end, size, get(0).getSymbol().getType().toString().c_str());
1871  append(str, end, size, ") ");
1872  get(1).toString(old, str, end, size);
1873  break;
1874 
1875  case EXISTS:
1876  append(str, end, size, "exists (");
1877  append(str, end, size, get(0).getSymbol().getName().c_str());
1878  append(str, end, size, ":");
1879  append(str, end, size, get(0).getSymbol().getType().toString().c_str());
1880  append(str, end, size, ") ");
1881  get(1).toString(old, str, end, size);
1882  break;
1883 
1884  case SUM:
1885  append(str, end, size, "sum (");
1886  append(str, end, size, get(0).getSymbol().getName().c_str());
1887  append(str, end, size, ":");
1888  append(str, end, size, get(0).getSymbol().getType().toString().c_str());
1889  append(str, end, size, ") ");
1890  get(1).toString(old, str, end, size);
1891  break;
1892 
1893  case SMC_CONTROL:
1894  append(str, end, size, "control[");
1895  appendBoundType(str, end, size, get(0));
1896  get(1).toString(old, str, end, size);
1897  append(str, end, size, "]: ");
1898  get(2).toString(old, str, end, size);
1899  break;
1900 
1901  case PO_CONTROL:
1902  append(str, end, size, "{ ");
1903  get(0).toString(old, str, end, size);
1904  append(str, end, size, "} control: ");
1905  get(1).toString(old, str, end, size);
1906  break;
1907 
1908  case EF_CONTROL:
1909  append(str, end, size, "E<> ");
1910  case CONTROL:
1911  append(str, end, size, "control: ");
1912  get(0).toString(old, str, end, size);
1913  break;
1914 
1915  case CONTROL_TOPT:
1916  append(str, end, size, "control_t*(");
1917  get(0).toString(old, str, end, size);
1918  append(str, end, size, ",");
1919  get(1).toString(old, str, end, size);
1920  append(str, end, size, "): ");
1921  get(2).toString(old, str, end, size);
1922  break;
1923 
1924  case CONTROL_TOPT_DEF1:
1925  append(str, end, size, "control_t*(");
1926  get(0).toString(old, str, end, size);
1927  append(str, end, size, "): ");
1928  get(1).toString(old, str, end, size);
1929  break;
1930 
1931  case CONTROL_TOPT_DEF2:
1932  append(str, end, size, "control_t*: ");
1933  get(0).toString(old, str, end, size);
1934  break;
1935 
1936  case SUP_VAR:
1937  append(str, end, size, "sup{");
1938  get(0).toString(old, str, end, size);
1939  append(str, end, size, "}: ");
1940  get(1).toString(old, str, end, size);
1941  break;
1942 
1943  case INF_VAR:
1944  append(str, end, size, "inf{");
1945  get(0).toString(old, str, end, size);
1946  append(str, end, size, "}: ");
1947  get(1).toString(old, str, end, size);
1948  break;
1949 
1950  case MITLFORMULA:
1951  append (str,end,size,"MITL: ");
1952  get(0).toString (old,str,end,size);
1953  break;
1954  case MITLRELEASE:
1955  case MITLUNTIL:
1956  get(0).toString (old,str,end,size);
1957  append (str,end,size,"U[");
1958  get(1).toString (old,str,end,size);
1959  append (str,end,size,";");
1960  get(2).toString (old,str,end,size);
1961  append (str,end,size,"]");
1962  get(3).toString (old,str,end,size);
1963  break;
1964 
1965  case MITLDISJ:
1966  get(0).toString (old,str,end,size);
1967  append (str,end,size,"\\/");
1968  get(1).toString (old,str,end,size);
1969  break;
1970  case MITLCONJ:
1971  get(0).toString (old,str,end,size);
1972  append (str,end,size,"/\\");
1973  get(1).toString (old,str,end,size);
1974  break;
1975  case MITLATOM:
1976  get(0).toString (old,str,end,size);
1977  break;
1978  case MITLNEXT:
1979  append (str,end,size,"X(");
1980  get(0).toString (old,str,end,size);
1981  append (str,end,size,")");
1982  break;
1983  case SPAWN:
1984  append (str,end,size,"SPAWN");
1985 
1986  break;
1987  case EXIT:
1988  append (str,end,size,"EXIT");
1989 
1990  break;
1991  case NUMOF:
1992 
1993  append (str,end,size,"numof(");
1994  get(0).toString(old,str,end,size);
1995  append (str,end,size,")");
1996  break;
1997  case FORALLDYNAMIC:
1998  append (str,end,size,"forall (");
1999  get(0).toString (old,str,end,size);
2000  append (str,end,size," : ");
2001  get(1).toString (old,str,end,size);
2002  append (str,end,size," )( ");
2003  get(2).toString (old,str,end,size);
2004  append (str,end,size,")");
2005  break;
2006  case SUMDYNAMIC:
2007  append (str,end,size,"sum (");
2008  get(0).toString (old,str,end,size);
2009  append (str,end,size," : ");
2010  get(1).toString (old,str,end,size);
2011  append (str,end,size," )( ");
2012  get(2).toString (old,str,end,size);
2013  append (str,end,size,")");
2014  break;
2015  case FOREACHDYNAMIC:
2016  append (str,end,size,"foreach (");
2017  get(0).toString (old,str,end,size);
2018  append (str,end,size," : ");
2019  get(1).toString (old,str,end,size);
2020  append (str,end,size," )( ");
2021  get(2).toString (old,str,end,size);
2022  append (str,end,size,")");
2023  break;
2024  case DYNAMICEVAL:
2025  get(1).toString (old,str,end,size);
2026  append (str,end,size,".");
2027  get(0).toString (old,str,end,size);
2028  break;
2029  case PROCESSVAR:
2030  get(0).toString (old,str,end,size);
2031  break;
2032  case MITLEXISTS:
2033  case EXISTSDYNAMIC:
2034  append (str,end,size,"exists (");
2035  get(0).toString (old,str,end,size);
2036  append (str,end,size," : ");
2037  get(1).toString (old,str,end,size);
2038  append (str,end,size," )( ");
2039  get(2).toString (old,str,end,size);
2040  append (str,end,size,")");
2041  break;
2042 
2043  default:
2044  throw std::runtime_error("Strange exception");
2045  }
2046 }
2047 
2049 {
2050  return data != NULL && e.data != NULL && data < e.data;
2051 }
2052 
2054 {
2055  return data == e.data;
2056 }
2057 
2058 
2062 std::string expression_t::toString(bool old) const
2063 {
2064  if (empty())
2065  {
2066  return std::string();
2067  }
2068  else
2069  {
2070  int size = 16;
2071  char *s, *end;
2072  s = end = new char[size];
2073  *s = 0;
2074  toString(old, s, end, size);
2075  std::string result(s);
2076  delete[] s;
2077  return result;
2078  }
2079 }
2080 
2081 void expression_t::collectPossibleWrites(set<symbol_t> &symbols) const
2082 {
2083  function_t *fun;
2084  symbol_t symbol;
2085  type_t type;
2086 
2087  if (empty())
2088  {
2089  return;
2090  }
2091 
2092  for (uint32_t i = 0; i < getSize(); i++)
2093  {
2094  get(i).collectPossibleWrites(symbols);
2095  }
2096 
2097  switch (getKind())
2098  {
2099  case ASSIGN:
2100  case ASSPLUS:
2101  case ASSMINUS:
2102  case ASSDIV:
2103  case ASSMOD:
2104  case ASSMULT:
2105  case ASSAND:
2106  case ASSOR:
2107  case ASSXOR:
2108  case ASSLSHIFT:
2109  case ASSRSHIFT:
2110  case POSTINCREMENT:
2111  case POSTDECREMENT:
2112  case PREINCREMENT:
2113  case PREDECREMENT:
2114  get(0).getSymbols(symbols);
2115  break;
2116 
2117  case FUNCALL:
2118  // Add all symbols which are changed by the function
2119  symbol = get(0).getSymbol();
2120  if (symbol.getType().isFunction() && symbol.getData())
2121  {
2122  fun = (function_t*)symbol.getData();
2123 
2124  symbols.insert(fun->changes.begin(), fun->changes.end());
2125 
2126  // Add arguments to non-constant reference parameters
2127  type = fun->uid.getType();
2128  for (uint32_t i = 1; i < min(getSize(), type.size()); i++)
2129  {
2130  if (type[i].is(REF) && !type[i].isConstant())
2131  {
2132  get(i).getSymbols(symbols);
2133  }
2134  }
2135  }
2136  break;
2137 
2138  default:
2139  break;
2140  }
2141 }
2142 
2143 void expression_t::collectPossibleReads(set<symbol_t> &symbols, bool collectRandom) const
2144 {
2145  function_t *fun;
2146  frame_t parameters;
2147  symbol_t symbol;
2148 
2149  if (empty())
2150  {
2151  return;
2152  }
2153 
2154  for (uint32_t i = 0; i < getSize(); i++)
2155  {
2156  get(i).collectPossibleReads(symbols);
2157  }
2158 
2159  switch (getKind())
2160  {
2161  case IDENTIFIER:
2162  symbols.insert(getSymbol());
2163  break;
2164 
2165  case FUNCALL:
2166  // Add all symbols which are used by the function
2167  symbol = get(0).getSymbol();
2168  if (symbol.getType().isFunction() && symbol.getData())
2169  {
2170  fun = (function_t*)symbol.getData();
2171  symbols.insert(fun->depends.begin(), fun->depends.end());
2172  }
2173  break;
2174 
2175  case RANDOM_F:
2176  case RANDOM_POISSON_F:
2177  if (collectRandom)
2178  {
2179  symbols.insert(symbol_t());
2180  }
2181  break;
2182  case RANDOM_ARCSINE_F:
2183  case RANDOM_BETA_F:
2184  case RANDOM_GAMMA_F:
2185  case RANDOM_NORMAL_F:
2186  case RANDOM_WEIBULL_F:
2187  if (collectRandom)
2188  {
2189  symbols.insert(symbol_t());
2190  symbols.insert(symbol_t());
2191  }
2192  break;
2193 
2194  case RANDOM_TRI_F:
2195  if (collectRandom)
2196  {
2197  symbols.insert(symbol_t());
2198  symbols.insert(symbol_t());
2199  symbols.insert(symbol_t());
2200  }
2201  break;
2202 
2203  default:
2204  break;
2205  }
2206 }
2207 
2208 
2210 {
2211  expression_t expr(CONSTANT, pos);
2212  expr.data->value = value;
2213  expr.data->type = type_t::createPrimitive(Constants::INT);
2214  return expr;
2215 }
2216 
2218 {
2219  expression_t expr(EXIT, pos);
2220  expr.data->value = 0;
2221  expr.data->type = type_t::createPrimitive(Constants::VOID_TYPE);
2222  return expr;
2223 }
2224 
2226 {
2227  expression_t expr(CONSTANT, pos);
2228  expr.data->doubleValue = value;
2229  expr.data->type = type_t::createPrimitive(Constants::DOUBLE);
2230  return expr;
2231 }
2232 
2234 {
2235  expression_t expr(IDENTIFIER, pos);
2236  expr.data->symbol = symbol;
2237  if (symbol != symbol_t())
2238  {
2239  expr.data->type = symbol.getType();
2240  }
2241  else
2242  {
2243  expr.data->type = type_t();
2244  }
2245  return expr;
2246 }
2247 
2249  kind_t kind, const vector<expression_t> &sub, position_t pos, type_t type)
2250 {
2251  expression_t expr(kind, pos);
2252  expr.data->value = sub.size();
2253  expr.data->sub.reserve(sub.size());
2254  expr.data->sub.assign(sub.begin(), sub.end());
2255  expr.data->type = type;
2256  return expr;
2257 }
2258 
2260  kind_t kind, expression_t sub, position_t pos, type_t type)
2261 {
2262  expression_t expr(kind, pos);
2263  expr.data->sub.push_back(sub);
2264  expr.data->type = type;
2265  return expr;
2266 }
2267 
2269  kind_t kind, expression_t left, expression_t right,
2270  position_t pos, type_t type)
2271 {
2272  expression_t expr(kind, pos);
2273  expr.data->sub.reserve(2);
2274  expr.data->sub.push_back(left);
2275  expr.data->sub.push_back(right);
2276  expr.data->type = type;
2277  return expr;
2278 }
2279 
2281  kind_t kind, expression_t e1, expression_t e2, expression_t e3,
2282  position_t pos, type_t type)
2283 {
2284  expression_t expr(kind, pos);
2285  expr.data->sub.reserve(3);
2286  expr.data->sub.push_back(e1);
2287  expr.data->sub.push_back(e2);
2288  expr.data->sub.push_back(e3);
2289  expr.data->type = type;
2290  return expr;
2291 }
2292 
2294  expression_t e, int32_t idx, position_t pos, type_t type)
2295 {
2296  expression_t expr(DOT, pos);
2297  expr.data->index = idx;
2298  expr.data->sub.push_back(e);
2299  expr.data->type = type;
2300  return expr;
2301 }
2302 
2305 {
2306  expression_t expr(SYNC, pos);
2307  expr.data->sync = s;
2308  expr.data->sub.push_back(e);
2309  return expr;
2310 }
2311 
2313 {
2314  expression_t expr(DEADLOCK, pos);
2315  expr.data->type = type_t::createPrimitive(CONSTRAINT);
2316  return expr;
2317 }
2318 
2319 ostream &operator<< (ostream &o, const expression_t &e)
2320 {
2321  o << e.toString();
2322  return o;
2323 }
static expression_t createDouble(double, position_t=position_t())
expression_t()
Default constructor.
Definition: expression.h:76
static bool isClock(expression_t expr)
Definition: typechecker.cpp:87
Constants::kind_t getKind() const
Returns the kind of the expression.
Definition: expression.cpp:182
bool resolve(const std::string &name, symbol_t &symbol)
Resolves a name in this frame or a parent frame.
Definition: symbols.cpp:446
void getSymbols(std::set< symbol_t > &symbols) const
Returns the set of symbols this expression might resolve into.
Definition: expression.cpp:775
static expression_t createExit(position_t=position_t())
bool changesVariable(const std::set< symbol_t > &) const
True if this expression can change any of the variables identified by the given symbols.
Definition: expression.cpp:844
int32_t getIndex() const
Returns the index field of this expression.
Definition: expression.cpp:635
bool empty() const
Returns true if this is an empty expression.
Definition: expression.cpp:671
expression_t clone() const
Make a shallow clone of the expression.
Definition: expression.cpp:81
std::set< symbol_t > changes
Variables changed by this function.
Definition: system.h:113
static void append(char *&str, char *&end, int &size, const char *s)
static expression_t createNary(Constants::kind_t, const std::vector< expression_t > &, position_t=position_t(), type_t=type_t())
Create an n-ary expression.
A reference to a symbol.
Definition: symbols.h:107
symbol_t getSymbol()
Returns the symbol of a variable reference.
Definition: expression.cpp:718
bool usesClock() const
Definition: expression.cpp:308
double getDoubleValue() const
Returns the value field of this expression.
Definition: expression.cpp:629
static type_t createPrimitive(Constants::kind_t, position_t=position_t())
Create a primitive type.
Definition: type.cpp:527
bool usesFP() const
Definition: expression.cpp:211
static const char * getBuiltinFunName(kind_t kind)
expression_t & operator=(const expression_t &)
Assignment operator.
Definition: expression.cpp:75
expression_t & operator[](uint32_t)
Returns the ith subexpression.
Definition: expression.cpp:647
static expression_t createDot(expression_t, int32_t=-1, position_t=position_t(), type_t=type_t())
Create a DOT expression.
std::set< symbol_t > depends
Variables the function depends on.
Definition: system.h:114
expression_t & get(uint32_t)
Returns the ith subexpression.
Definition: expression.cpp:659
expression_t subst(symbol_t, expression_t) const
Definition: expression.cpp:153
static expression_t createUnary(Constants::kind_t, expression_t, position_t=position_t(), type_t=type_t())
Create a unary expression.
std::ostream & operator<<(std::ostream &os, const SignalFlow::strs_t &s)
Definition: signalflow.h:189
const position_t & getPosition() const
Returns the position of this expression.
Definition: expression.cpp:188
bool isConstant() const
Returns true if and only if all elements of the type are constant.
Definition: type.cpp:375
static string symbol(const char *str)
Extracts the alpha-numerical symbol used for variable/type identifiers.
Definition: xmlreader.cpp:107
std::string toString(bool old=false) const
Returns a string representation of the expression.
bool isFunction() const
Shortcut for is(FUNCTION).
Definition: type.h:208
static expression_t createTernary(Constants::kind_t, expression_t, expression_t, expression_t, position_t=position_t(), type_t=type_t())
Create a ternary expression.
bool dependsOn(const std::set< symbol_t > &) const
True if the evaluation of this expression depends on any of the symbols in the given set...
Definition: expression.cpp:859
if(!(yy_init))
Definition: lexer.cc:1042
A reference to a frame.
Definition: symbols.h:183
void collectPossibleWrites(std::set< symbol_t > &) const
A reference to a type.
Definition: type.h:93
type_t getType() const
Returns the type of this symbol.
Definition: symbols.cpp:205
static expression_t createDeadlock(position_t=position_t())
Create a DEADLOCK expression.
size_t size() const
Returns the number of children.
Definition: type.cpp:81
symbol_t uid
The symbol of the function.
Definition: system.h:112
std::string getRecordLabel(size_t i) const
Returns the label of the &#39;th field of a record.
Definition: type.cpp:253
expression_t deeperClone() const
Makes a deep clone of the expression.
Definition: expression.cpp:92
A reference to an expression.
Definition: expression.h:70
bool hasDynamicSub() const
Definition: expression.cpp:353
Information about a function.
Definition: system.h:110
bool isDynamic() const
Definition: expression.cpp:329
type_t getType() const
Returns the type of the expression.
Definition: expression.cpp:611
void * getData()
Returns the user data of this symbol.
Definition: symbols.cpp:216
virtual int32_t accept(StatementVisitor *visitor)=0
int32_t getValue() const
Returns the value field of this expression.
Definition: expression.cpp:623
static void ensure(char *&str, char *&end, int &size, int len)
size_t getSize() const
Returns the number of subexpression.
Definition: expression.cpp:379
~expression_t()
Destructor.
Definition: expression.cpp:178
bool is(Constants::kind_t kind) const
Returns true if the type has kind kind or if type is a prefix, RANGE or REF type and the getChild()...
Definition: type.cpp:176
Definition: lexer.cc:817
static expression_t createSync(expression_t, Constants::synchronisation_t, position_t=position_t())
Create a SYNC expression.
bool isTrue() const
Definition: expression.cpp:676
static expression_t createConstant(int32_t, position_t=position_t())
Create a CONSTANT expression.
void setType(type_t)
Sets the type of the expression.
Definition: expression.cpp:617
Constants::synchronisation_t getSync() const
Returns the synchronisation type of SYNC operations.
Definition: expression.cpp:641
static expression_t createBinary(Constants::kind_t, expression_t, expression_t, position_t=position_t(), type_t=type_t())
Create a binary expression.
void collectPossibleReads(std::set< symbol_t > &, bool collectRandom=false) const
bool operator<(const expression_t) const
Less-than operator.
bool checkForFP(Statement *s)
Definition: expression.cpp:209
bool isRecord() const
Shortcut for is(RECORD).
Definition: type.h:238
static expression_t createIdentifier(symbol_t, position_t=position_t())
Create an IDENTIFIER expression.
bool isReferenceTo(const std::set< symbol_t > &) const
Returns true if this expression is a reference to a symbol in the given set.
Definition: expression.cpp:836
bool isProcess() const
Shortcut for is(PROCESS).
Definition: type.h:211
bool operator==(const expression_t) const
Equality operator.
bool equal(const expression_t &) const
Equality operator.
Definition: expression.cpp:685
bool changesAnyVariable() const
True if this expression can change any variable at all.
Definition: expression.cpp:852