src/Interpreter/alloysig.cc

   1 #include "alloysig.h"
   2 #include "set.h"
   3
   4 bool AlloyBoolSig::encodeAbs = true;
   5 bool AlloySetSig::encodeAbs = true;
   6 bool AlloyElementSig::encodeAbs = true;
   7
   8 AlloyBoolSig::AlloyBoolSig(uint id):
   9         ValuedSignature(id)
  10 {
  11 }
  12
  13 string AlloyBoolSig::toString() const{
  14         return "Boolean" + to_string(id) + ".value";
  15 }
  16
  17 string AlloyBoolSig::getSignature() const{
  18         string str;
  19         if(encodeAbs){
  20                 encodeAbs = false;
  21                 str += getAbsSignature();
  22         }
  23         str += "one sig Boolean" + to_string(id) + " extends AbsBool {}";
  24         return str;
  25 }
  26
  27 string AlloyBoolSig::getAbsSignature() const{
  28         string str;
  29         if(AlloySetSig::encodeAbs){
  30                 AlloySetSig::encodeAbs = false;
  31                 str += "abstract sig AbsSet {\
  32                 domain: set Int\
  33                 }\n";
  34         }
  35         str +="one sig BooleanSet extends AbsSet {}{\n\
  36         domain = 0 + 1 \n\
  37         }\n\
  38         abstract sig AbsBool {\
  39         value: Int\
  40         }{\n\
  41         value in BooleanSet.domain\n\
  42         }\n";
  43         return str;
  44 }
  45
  46 AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig):
  47         ValuedSignature(id),
  48         ssig(_ssig)
  49 {
  50 }
  51
  52 string AlloyElementSig::toString() const{
  53         return "Element" + to_string(id) + ".value";
  54 }
  55
  56 string AlloyElementSig::getSignature() const{
  57         string str;
  58         if(encodeAbs){
  59                 encodeAbs = false;
  60                 str += getAbsSignature();
  61         }
  62         str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\
  63                 value in " + *ssig + "\n\
  64                 }";
  65         return str;
  66 }
  67
  68 string AlloyElementSig::getAbsSignature() const{
  69         return "abstract sig AbsElement {\n\
  70                 value: Int\n\
  71                 }\n";
  72
  73 }
  74
  75 AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
  76         ASSERT(set->getSize() > 0);
  77         domain = to_string(set->getElement(0));
  78         for(uint i=1; i< set->getSize(); i++){
  79                 domain += " + " + to_string(set->getElement(i));
  80         }
  81 }
  82
  83 string AlloySetSig::toString() const{
  84         return "Set" + to_string(id) + ".domain";
  85 }
  86
  87 string AlloySetSig::getSignature() const{
  88         string str;
  89         if(encodeAbs){
  90                 encodeAbs = false;
  91                 str += getAbsSignature();
  92         }
  93         str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\
  94                 domain = " + domain + "\n\
  95                 }";
  96         return str;
  97 }
  98
  99 string AlloySetSig::getAbsSignature() const{
 100         return "abstract sig AbsSet {\n\
 101                 domain: set Int\n\
 102                 }\n";
 103
 104 }