00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00027 #include <semantics.h>
00028
00029 void convex_e::read(char *c)
00030 {
00031 switch(c[0])
00032 {
00033 case 'V':
00034 e = c_concave;
00035 break;
00036 case 'X':
00037 e = c_convex;
00038 break;
00039 case 'L':
00040 e = c_linear;
00041 break;
00042 case 'M':
00043 e = c_maybe;
00044 break;
00045 default:
00046 throw "malformed convexity info: wrong type";
00047 }
00048 unsigned int t;
00049 if(sscanf(c+1,"%u",&t) != 1)
00050 throw "malformed convexity info: tested is not an integer";
00051 tested = (uint16_t)t;
00052 }
00053
00054 const char* semantics::print_tristate(const tristate& x) const
00055 {
00056 if(x == t_true) return "T";
00057 if(x == t_false) return "F";
00058 return "M";
00059 }
00060
00061 tristate semantics::read_tristate(char c) const
00062 {
00063 if(c == 'T') return t_true;
00064 if(c == 'F') return t_false;
00065 return t_maybe;
00066 }
00067
00068 const char* semantics::print_type_annotation(const type_annotation& x) const
00069 {
00070 switch(x)
00071 {
00072 case v_exists:
00073 return "E";
00074 case v_forall:
00075 return "A";
00076 case v_free:
00077 return "F";
00078 case v_stochastic:
00079 return "S";
00080 }
00081
00082 return "";
00083 }
00084
00085 type_annotation semantics::read_type_annotation(char c) const
00086 {
00087 switch(c)
00088 {
00089 case 'A':
00090 return v_forall;
00091 case 'F':
00092 return v_free;
00093 case 'S':
00094 return v_stochastic;
00095 }
00096 return v_exists;
00097 }
00098
00099 const char* semantics::print_activity_descr(const activity_descr& x) const
00100 {
00101 switch(x)
00102 {
00103 case a_redundant:
00104 return "R";
00105 case a_active_lo:
00106 return "l";
00107 case a_active_lo_red:
00108 return "L";
00109 case a_active_hi:
00110 return "h";
00111 case a_active_hi_red:
00112 return "H";
00113 case a_active:
00114 return "a";
00115 case a_active_red:
00116 return "A";
00117 }
00118
00119 return "";
00120 }
00121
00122 activity_descr semantics::read_activity_descr(char c) const
00123 {
00124 switch(c)
00125 {
00126 case 'A':
00127 return a_active_red;
00128 case 'H':
00129 return a_active_hi_red;
00130 case 'L':
00131 return a_active_lo_red;
00132 case 'R':
00133 return a_redundant;
00134 case 'a':
00135 return a_active;
00136 case 'h':
00137 return a_active_hi;
00138 case 'l':
00139 return a_active_lo;
00140 }
00141 return a_active;
00142 }
00143
00144 void semantics::read(char *c)
00145 {
00146 try
00147 {
00148 for(; c;)
00149 {
00150 char *ct;
00151
00152 ct = strsep(&c, ",");
00153 ct += strspn(ct, " \t");
00154 switch(ct[0])
00155 {
00156 case 'C':
00157 if(ct[1] != '=')
00158 throw "malformed semantics C expression: `=' missing";
00159 property_flags.c_info.read(ct+2);
00160 break;
00161 case 'P':
00162 if(ct[1] != '=')
00163 throw "malformed semantics P expression: `=' missing";
00164 property_flags.separable = read_tristate(ct[2]);
00165 property_flags.act = read_activity_descr(ct[3]);
00166 property_flags.is_at_any_bound = (ct[4] == 'T' ? true : false);
00167 break;
00168 case 'N':
00169 if(ct[1] != '=')
00170 throw "malformed semantics N expression: `=' missing";
00171 annotation_flags.kj = (ct[2] == 'T' ? true : false);
00172 annotation_flags.integer = (ct[3] == 'T' ? true : false);
00173 annotation_flags.hard = (ct[4] == 'T' ? true : false);
00174 annotation_flags.type = read_type_annotation(ct[5]);
00175 break;
00176 case 'I':
00177 if(ct[1] != '=')
00178 throw "malformed semantics I expression: `=' missing";
00179 info_flags.has_0chnbase = read_tristate(ct[3]);
00180 break;
00181 case 'A':
00182 if(ct[1] != '=')
00183 throw "malformed semantics A expression: `=' missing";
00184 if(sscanf(ct+2, "%d", &addinfo) != 1)
00185 throw "malformed semantics A expression: no integer";
00186 break;
00187 case 'B':
00188 if(ct[1] != '=')
00189 throw "malformed semantics B expression: `=' missing";
00190 if(sscanf(ct+2, "%u", &_0chnbase) != 1)
00191 throw "malformed semantics B expression: no integer";
00192 break;
00193 case 'G':
00194 if(ct[1] != '=')
00195 throw "malformed semantics G expression: `=' missing";
00196 if(sscanf(ct+2, "%d", °ree) != 1)
00197 throw "malformed semantics G expression: no integer";
00198 break;
00199 case 'D':
00200 if(ct[1] != '=')
00201 throw "malformed semantics D expression: `=' missing";
00202 if(sscanf(ct+2, "%d", &dim) != 1)
00203 throw "malformed semantics D expression: no integer";
00204 break;
00205 case 'S':
00206 if(ct[1] != '=')
00207 throw "malformed semantics S expression: `=' missing";
00208 if(sscanf(ct+2, "%d", &stage) != 1)
00209 throw "malformed semantics S expression: no integer";
00210 break;
00211 default:
00212 throw "malformed semantics expression: wrong type";
00213 break;
00214 }
00215 }
00216 }
00217 catch(char *str)
00218 {
00219 std::cerr << "Error: " << str << std::endl;
00220 std::terminate();
00221 }
00222 }
00223
00224 std::ostream& operator<< (std::ostream& o, const semantics& __s)
00225 {
00226 o << "C=";
00227 o << __s.property_flags.c_info;
00228 o << ",P=";
00229 o << __s.print_tristate(__s.property_flags.separable);
00230 o << __s.print_activity_descr(__s.property_flags.act);
00231 o << (__s.property_flags.is_at_any_bound ? "T" : "F");
00232 o << ",N=";
00233 o << (__s.annotation_flags.kj ? "T" : "F");
00234 o << (__s.annotation_flags.integer ? "T" : "F");
00235 o << (__s.annotation_flags.hard ? "T" : "F");
00236 o << __s.print_type_annotation(__s.annotation_flags.type);
00237 o << ",I=";
00238 o << __s.print_tristate(__s.info_flags.has_0chnbase);
00239 o << ",A=" << __s.addinfo;
00240 o << ",B=" << __s._0chnbase;
00241 o << ",G=" << __s.degree;
00242 o << ",D=" << __s.dim;
00243 o << ",S=" << __s.stage;
00244 return o;
00245 }