Revision 7
Added by Willibald K. over 8 years ago
| OoaCADPVisitor.java | ||
|---|---|---|
| 1 |
/**
|
|
| 2 |
*
|
|
| 3 |
* OOAS Compiler
|
|
| 4 |
*
|
|
| 5 |
* Copyright 2015, AIT Austrian Institute of Technology.
|
|
| 6 |
* This code is based on the C# Version of the OOAS Compiler, which is
|
|
| 7 |
* copyright 2015 by the Institute of Software Technology, Graz University
|
|
| 8 |
* of Technology with portions copyright by the AIT Austrian Institute of
|
|
| 9 |
* Technology. All rights reserved.
|
|
| 10 |
*
|
|
| 11 |
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
|
|
| 12 |
*
|
|
| 13 |
* If you modify the file please update the list of contributors below to in-
|
|
| 14 |
* clude your name. Please also stick to the coding convention of using TABs
|
|
| 15 |
* to do the basic (block-level) indentation and spaces for anything after
|
|
| 16 |
* that. (Enable the display of special chars and it should be pretty obvious
|
|
| 17 |
* what this means.) Also, remove all trailing whitespace.
|
|
| 18 |
*
|
|
| 19 |
* Contributors:
|
|
| 20 |
* Willibald Krenn (AIT)
|
|
| 21 |
* Stephan Zimmerer (AIT)
|
|
| 22 |
* Markus Demetz (AIT)
|
|
| 23 |
* Christoph Czurda (AIT)
|
|
| 24 |
*
|
|
| 25 |
*/
|
|
| 1 |
/** |
|
| 2 |
* |
|
| 3 |
* OOAS Compiler |
|
| 4 |
* |
|
| 5 |
* Copyright 2015, AIT Austrian Institute of Technology. |
|
| 6 |
* This code is based on the C# Version of the OOAS Compiler, which is |
|
| 7 |
* copyright 2015 by the Institute of Software Technology, Graz University |
|
| 8 |
* of Technology with portions copyright by the AIT Austrian Institute of |
|
| 9 |
* Technology. All rights reserved. |
|
| 10 |
* |
|
| 11 |
* SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED. |
|
| 12 |
* |
|
| 13 |
* If you modify the file please update the list of contributors below to in- |
|
| 14 |
* clude your name. Please also stick to the coding convention of using TABs |
|
| 15 |
* to do the basic (block-level) indentation and spaces for anything after |
|
| 16 |
* that. (Enable the display of special chars and it should be pretty obvious |
|
| 17 |
* what this means.) Also, remove all trailing whitespace. |
|
| 18 |
* |
|
| 19 |
* Contributors: |
|
| 20 |
* Willibald Krenn (AIT) |
|
| 21 |
* Stephan Zimmerer (AIT) |
|
| 22 |
* Markus Demetz (AIT) |
|
| 23 |
* Christoph Czurda (AIT) |
|
| 24 |
* |
|
| 25 |
*/ |
|
| 26 | 26 |
|
| 27 | 27 |
|
| 28 |
package org.momut.ooas.codegen.cadp; |
|
| 29 |
|
|
| 30 |
import java.util.ArrayList; |
|
| 31 |
import java.util.Date; |
|
| 32 |
import java.util.List; |
|
| 28 |
package org.momut.ooas.codegen.cadp; |
|
| 33 | 29 |
|
| 30 |
import java.util.ArrayList; |
|
| 31 |
import java.util.Date; |
|
| 32 |
import java.util.List; |
|
| 33 |
|
|
| 34 | 34 |
import org.momut.ooas.Version; |
| 35 | 35 |
import org.momut.ooas.ast.identifiers.AttributeIdentifier; |
| 36 | 36 |
import org.momut.ooas.ast.identifiers.FunctionIdentifier; |
| ... | ... | |
| 49 | 49 |
import org.momut.ooas.codegen.OoasCodeEmitter; |
| 50 | 50 |
import org.momut.ooas.parser.ParserState; |
| 51 | 51 |
import org.momut.ooas.visitors.OoaCompleteAstTraversalVisitor; |
| 52 |
|
|
| 53 |
|
|
| 54 |
/* |
|
| 55 |
* OoaCADPVisitor |
|
| 56 |
* |
|
| 57 |
*/ |
|
| 58 |
|
|
| 59 |
public final class OoaCADPVisitor extends OoaCompleteAstTraversalVisitor |
|
| 60 |
{
|
|
| 61 |
final static int s_codeGenVersion = 10; |
|
| 62 |
|
|
| 63 |
private OoasCodeEmitter m_output; |
|
| 64 |
private final List<AttributeIdentifier> m_statevector; |
|
| 65 |
private final int GraphImplementationVersion = 24; |
|
| 66 |
private final List<NamedActionIdentifier> actions = new ArrayList<NamedActionIdentifier>(); |
|
| 67 |
private final List<MethodIdentifier> methods = new ArrayList<MethodIdentifier>(); |
|
| 68 |
// private final String m_AttributePre; |
|
| 69 |
public int m_internalActionNumber = 0; |
|
| 70 |
|
|
| 71 |
public static int getUIntHashCode(Object o) {
|
|
| 72 |
int hash = o.hashCode(); |
|
| 73 |
if (hash >= 0) |
|
| 74 |
return hash; |
|
| 75 |
if (hash == Integer.MIN_VALUE) |
|
| 76 |
hash +=1; |
|
| 77 |
return -hash; |
|
| 78 |
} |
|
| 79 |
|
|
| 80 |
/// <summary> |
|
| 81 |
/// Dumps a comment containing all the version information |
|
| 82 |
/// </summary> |
|
| 83 |
private void DumpHeader(OoasCodeEmitter m_output) |
|
| 84 |
{
|
|
| 85 |
m_output.AppendLine(); |
|
| 86 |
m_output.AppendLine("/* Argos Generated");
|
|
| 87 |
m_output.AppendLine(Version.asString()); |
|
| 88 |
m_output.AppendLine(String.format(" Code-Gen Version: %s", s_codeGenVersion));
|
|
| 89 |
m_output.Append(" Generated: "); m_output.AppendLine((new Date()).toString());
|
|
| 90 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 91 |
m_output.AppendLine(); |
|
| 92 |
m_output.AppendLine(" assumed data-type sizes:");
|
|
| 93 |
for( final String x : CadpType.sizeOfTypes().keySet()) |
|
| 94 |
m_output.AppendLine(String.format("%s: %s", new Object[] { x, CadpType.sizeOfTypes().get(x).toString() }));
|
|
| 95 |
m_output.AppendLine("");
|
|
| 96 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 97 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 98 |
m_output.AppendLine("*/");
|
|
| 99 |
} |
|
| 100 |
|
|
| 101 |
/// <summary> |
|
| 102 |
/// Prints out general definitions, includes |
|
| 103 |
/// </summary> |
|
| 104 |
private void DumpDefinitions(OoasCodeEmitter m_output) |
|
| 105 |
{
|
|
| 106 |
// write Graph version and include header |
|
| 107 |
m_output.AppendLine("/*define next symbol if you want to see named internal actions (otherwise they are mapped to 'i')*/");
|
|
| 108 |
m_output.AppendLine("#define ALL_ACTIONS_VISIBLE");
|
|
| 109 |
m_output.AppendLine("/*define next symbol if you need to re-eval internal (hidden) states - attention: memory leaks*/");
|
|
| 110 |
m_output.AppendLine("//#define UNLIMITED_REEVAL");
|
|
| 111 |
m_output.AppendLine(String.format("#define CAESAR_GRAPH_IMPLEMENTATION %s", GraphImplementationVersion));
|
|
| 112 |
m_output.AppendLine("#include \"caesar_graph.h\"");
|
|
| 113 |
m_output.AppendLine("#include \"argos_runtime.h\"");
|
|
| 114 |
m_output.AppendLine("#if defined(unix) || defined(__MACH__)");
|
|
| 115 |
m_output.AppendLine("#define UNIXPACK __attribute__((__packed__))");
|
|
| 116 |
m_output.AppendLine("#undef WINDOWSPACK");
|
|
| 117 |
m_output.AppendLine("#include <netinet/in.h>");
|
|
| 118 |
m_output.AppendLine("#else");
|
|
| 119 |
m_output.AppendLine("#include <winsock.h>");
|
|
| 120 |
m_output.AppendLine("#define WINDOWSPACK");
|
|
| 121 |
m_output.AppendLine("#define UNIXPACK");
|
|
| 122 |
m_output.AppendLine("#endif");
|
|
| 123 |
|
|
| 124 |
m_output.AppendLine(" typedef unsigned long CAESAR_TYPE_WORD;");
|
|
| 125 |
m_output.AppendLine(" #define CAESAR_WORD_SIZE (sizeof (CAESAR_TYPE_WORD))");
|
|
| 126 |
m_output.AppendLine(" #define CAESAR_FULL_MASK ((CAESAR_TYPE_WORD) ~0)");
|
|
| 127 |
|
|
| 128 |
m_output.AppendLine("");
|
|
| 129 |
m_output.AppendLine("unsigned char CALC_INVALID = 0;");
|
|
| 130 |
|
|
| 131 |
m_output.AppendLine("");
|
|
| 132 |
m_output.AppendLine("void CAESAR_TERMINATE (int CAESAR_ABORT)");
|
|
| 133 |
m_output.AppendLine("{printf(\"aborted...\"); abort();}");
|
|
| 134 |
m_output.AppendLine("");
|
|
| 135 |
} |
|
| 136 |
/// <summary> |
|
| 137 |
/// Prints out compiler String |
|
| 138 |
/// </summary> |
|
| 139 |
private void DumpCompilerString() |
|
| 140 |
{
|
|
| 141 |
m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_GRAPH_COMPILER ()");
|
|
| 142 |
lp(); |
|
| 143 |
m_output.AppendLine(" return (\"ARGOS\");");
|
|
| 144 |
rp(); |
|
| 145 |
} |
|
| 146 |
|
|
| 147 |
/// <summary> |
|
| 148 |
/// Prints out compiler version |
|
| 149 |
/// </summary> |
|
| 150 |
private void DumpCompilerVersion() |
|
| 151 |
{
|
|
| 152 |
m_output.AppendLine("CAESAR_TYPE_VERSION CAESAR_GRAPH_VERSION ()");
|
|
| 153 |
lp(); |
|
| 154 |
m_output.AppendLine(" return (" + Version.s_releaseMajor + "." + Version.s_releaseMinor + ");");
|
|
| 155 |
rp(); |
|
| 156 |
} |
|
| 157 |
/// <summary> |
|
| 158 |
/// Exports a function returning the maximum number of formats for states. |
|
| 159 |
/// Exports a const for the default format. |
|
| 160 |
/// Exports a function CAESAR_FORMAT_STATE (default cadp implementation). |
|
| 161 |
/// </summary> |
|
| 162 |
private void DumpFormat() |
|
| 163 |
{
|
|
| 164 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_MAX_FORMAT_STATE ()");
|
|
| 165 |
lp(); |
|
| 166 |
m_output.AppendLine(" return (0);");
|
|
| 167 |
rp(); |
|
| 168 |
|
|
| 169 |
line(); |
|
| 170 |
m_output.AppendLine("static CAESAR_TYPE_NATURAL CAESAR_CURRENT_STATE_FORMAT = 0;");
|
|
| 171 |
|
|
| 172 |
|
|
| 173 |
line(); |
|
| 174 |
m_output.AppendLine("void CAESAR_FORMAT_STATE (CAESAR_TYPE_NATURAL CAESAR_FORMAT)");
|
|
| 175 |
lp(); |
|
| 176 |
m_output.AppendLine(" if (CAESAR_FORMAT > CAESAR_MAX_FORMAT_STATE ()) ");
|
|
| 177 |
m_output.AppendLine(" printf(\"#233 bug during simulation:\\n unknown state printing format\\n\");");
|
|
| 178 |
m_output.AppendLine(" else");
|
|
| 179 |
m_output.AppendLine(" CAESAR_CURRENT_STATE_FORMAT = CAESAR_FORMAT;");
|
|
| 180 |
m_output.AppendLine("}");
|
|
| 181 |
} |
|
| 182 |
|
|
| 183 |
|
|
| 184 |
/// <summary> |
|
| 185 |
/// Exports a function to print a state header. (standard cadp implementation) |
|
| 186 |
/// </summary> |
|
| 187 |
private void DumpStateHeader() |
|
| 188 |
{
|
|
| 189 |
m_output.AppendLine("void CAESAR_PRINT_STATE_HEADER (CAESAR_TYPE_FILE CAESAR_FILE)");
|
|
| 190 |
m_output.AppendLine("{");
|
|
| 191 |
m_output.AppendLine(" switch (CAESAR_CURRENT_STATE_FORMAT) {");
|
|
| 192 |
m_output.AppendLine(" case 0:");
|
|
| 193 |
m_output.Append(" fprintf (CAESAR_FILE, \"\\t marquage = {\");");
|
|
| 194 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \"unite 0}\\n\");");
|
|
| 195 |
m_output.AppendLine(" break;");
|
|
| 196 |
m_output.AppendLine(" default:");
|
|
| 197 |
m_output.AppendLine(" {");
|
|
| 198 |
m_output.AppendLine(" printf(\"#233 bug during simulation:\\n unknown state printing format\\n\");");
|
|
| 199 |
m_output.AppendLine(" }");
|
|
| 200 |
m_output.AppendLine(" break;");
|
|
| 201 |
m_output.AppendLine(" }");
|
|
| 202 |
m_output.AppendLine("}");
|
|
| 203 |
} |
|
| 204 |
|
|
| 205 |
|
|
| 206 |
|
|
| 207 |
|
|
| 208 |
/// <summary> |
|
| 209 |
/// Main Routine, dumps an action system |
|
| 210 |
/// </summary> |
|
| 211 |
/// <param name="ooActionSystemType">action system to write out</param> |
|
| 212 |
private void Dump(OoActionSystemType ooActionSystemType) |
|
| 213 |
{
|
|
| 214 |
|
|
| 215 |
|
|
| 216 |
// write name of type we print out. |
|
| 217 |
m_output.AppendLine(); |
|
| 218 |
m_output.Append("/* Type: "); m_output.Append(ooActionSystemType.identifier().tokenText());
|
|
| 219 |
m_output.AppendLine(" */");
|
|
| 220 |
m_output.AppendLine(); |
|
| 221 |
|
|
| 222 |
// export state variables |
|
| 223 |
DefineCadpState(ooActionSystemType); |
|
| 224 |
|
|
| 225 |
// export compiler String function |
|
| 226 |
line(); |
|
| 227 |
DumpCompilerString(); |
|
| 228 |
|
|
| 229 |
// export compiler version function |
|
| 230 |
line(); |
|
| 231 |
DumpCompilerVersion(); |
|
| 232 |
|
|
| 233 |
// export state comparison function |
|
| 234 |
line(); |
|
| 235 |
DefineCompareCadpStates(); |
|
| 236 |
|
|
| 237 |
// export a state hash function |
|
| 238 |
line(); |
|
| 239 |
DefineCadpStateHash(); |
|
| 240 |
|
|
| 241 |
|
|
| 242 |
line(); |
|
| 243 |
DumpFormat(); |
|
| 244 |
|
|
| 245 |
line(); |
|
| 246 |
DumpStateHeader(); |
|
| 247 |
|
|
| 248 |
line(); |
|
| 249 |
DefineCadpPrintState(); |
|
| 250 |
|
|
| 251 |
line(); |
|
| 252 |
DefineCadpPrintDeltaState(); |
|
| 253 |
|
|
| 254 |
|
|
| 255 |
line(); |
|
| 256 |
DefineCadpLabel(ooActionSystemType); // populates actions list |
|
| 257 |
|
|
| 258 |
line(); |
|
| 259 |
m_output.AppendLine(); |
|
| 260 |
m_output.AppendLine("typedef struct CAESAR_STRUCT_ALIGNMENT_LABEL {");
|
|
| 261 |
m_output.AppendLine(" char CAESAR_BYTE;");
|
|
| 262 |
m_output.AppendLine(" CAESAR_BODY_LABEL CAESAR_L;");
|
|
| 263 |
m_output.AppendLine("} CAESAR_BODY_ALIGNMENT_LABEL;");
|
|
| 264 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_ALIGNMENT_LABEL = sizeof (CAESAR_BODY_ALIGNMENT_LABEL) - sizeof (CAESAR_BODY_LABEL);");
|
|
| 265 |
|
|
| 266 |
|
|
| 267 |
line(); |
|
| 268 |
m_output.AppendLine(); |
|
| 269 |
m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_VISIBLE_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 270 |
m_output.AppendLine("{");
|
|
| 271 |
m_output.AppendLine(" return 1;");
|
|
| 272 |
m_output.AppendLine("}");
|
|
| 273 |
|
|
| 274 |
|
|
| 275 |
line(); |
|
| 276 |
m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_GATE_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 277 |
lp(); |
|
| 278 |
m_output.AppendLine(String.format(" if(CAESAR_L->CAESAR_TRANSITION_NUMBER < %1$s)", this.actions.size()));
|
|
| 279 |
m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
|
|
| 280 |
m_output.AppendLine(" return CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION ? CAESAR_GATE[INTERNAL_ACTION_NUMBER] : CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
|
|
| 281 |
m_output.AppendLine("#else");
|
|
| 282 |
m_output.AppendLine(" return CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
|
|
| 283 |
m_output.AppendLine("#endif");
|
|
| 284 |
m_output.AppendLine(" else");
|
|
| 285 |
m_output.AppendLine(" {printf(\"#233 bug during simulation:\\n unknown gate number\\n\"); CAESAR_TERMINATE(1);}");
|
|
| 286 |
m_output.AppendLine(" return \"\";");
|
|
| 287 |
rp(); |
|
| 288 |
|
|
| 289 |
|
|
| 290 |
line(); |
|
| 291 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_CARDINAL_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 292 |
lp(); |
|
| 293 |
m_output.AppendLine(String.format(" if(CAESAR_L->CAESAR_TRANSITION_NUMBER < %1$s)", this.actions.size()));
|
|
| 294 |
m_output.AppendLine(" return CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
|
|
| 295 |
m_output.AppendLine(" else");
|
|
| 296 |
m_output.AppendLine(" {printf(\"#233 bug during simulation:\\n unknown gate number\\n\"); CAESAR_TERMINATE(1);}");
|
|
| 297 |
m_output.AppendLine("return 0;");
|
|
| 298 |
rp(); |
|
| 299 |
|
|
| 300 |
|
|
| 301 |
line(); |
|
| 302 |
DefineCadpGetStringLabel(); |
|
| 303 |
|
|
| 304 |
|
|
| 305 |
line(); |
|
| 306 |
DefineCadpCompareLabel(); |
|
| 307 |
|
|
| 308 |
line(); |
|
| 309 |
DefineCadpHashLabel(); |
|
| 310 |
|
|
| 311 |
|
|
| 312 |
line(); |
|
| 313 |
DefineCadpPrintLabel(); |
|
| 314 |
|
|
| 315 |
|
|
| 316 |
line(); |
|
| 317 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_MAX_FORMAT_LABEL ()");
|
|
| 318 |
lp(); |
|
| 319 |
m_output.AppendLine(" return (0);");
|
|
| 320 |
rp(); |
|
| 321 |
m_output.AppendLine(); |
|
| 322 |
m_output.AppendLine("static CAESAR_TYPE_NATURAL CAESAR_CURRENT_LABEL_FORMAT = 0;");
|
|
| 323 |
|
|
| 324 |
|
|
| 325 |
|
|
| 326 |
line(); |
|
| 327 |
m_output.AppendLine("void CAESAR_FORMAT_LABEL (CAESAR_TYPE_NATURAL CAESAR_FORMAT)");
|
|
| 328 |
lp(); |
|
| 329 |
m_output.AppendLine(" if (CAESAR_FORMAT > CAESAR_MAX_FORMAT_LABEL ()){");
|
|
| 330 |
lp(); |
|
| 331 |
m_output.AppendLine(" printf(\"#234 bug during simulation:\\n unknown label printing format\\n\");");
|
|
| 332 |
rp(); |
|
| 333 |
rp(); m_output.Append(" else CAESAR_CURRENT_LABEL_FORMAT = CAESAR_FORMAT;");
|
|
| 334 |
rp(); |
|
| 335 |
|
|
| 336 |
|
|
| 337 |
|
|
| 338 |
line(); |
|
| 339 |
m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_INFORMATION_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 340 |
lp(); |
|
| 341 |
m_output.AppendLine(" static char CAESAR_RESULT [11];");
|
|
| 342 |
m_output.AppendLine(" switch (CAESAR_CURRENT_LABEL_FORMAT) ");
|
|
| 343 |
m_output.AppendLine(" {");
|
|
| 344 |
m_output.AppendLine(" case 0:");
|
|
| 345 |
m_output.AppendLine(" sprintf (CAESAR_RESULT, \"%u\", CAESAR_L->CAESAR_TRANSITION_NUMBER);");
|
|
| 346 |
m_output.AppendLine(" return (CAESAR_RESULT);");
|
|
| 347 |
m_output.AppendLine(" default:");
|
|
| 348 |
m_output.AppendLine(" {");
|
|
| 349 |
m_output.AppendLine(" printf(\"#234 bogue pendant la simulation :\\n format d'impression inconnu pour les etiquettes\\n\");");
|
|
| 350 |
m_output.AppendLine(" }");
|
|
| 351 |
m_output.AppendLine(" return (\"\");");
|
|
| 352 |
m_output.AppendLine(" }");
|
|
| 353 |
rp(); |
|
| 354 |
|
|
| 355 |
|
|
| 356 |
/// |
|
| 357 |
/// START STATE |
|
| 358 |
/// |
|
| 359 |
line(); |
|
| 360 |
line(); |
|
| 361 |
DefineCadpStartState(); |
|
| 362 |
|
|
| 363 |
|
|
| 364 |
/// |
|
| 365 |
/// Dump Methods |
|
| 366 |
/// |
|
| 367 |
for (final MethodIdentifier method: methods) |
|
| 368 |
{
|
|
| 369 |
line(); |
|
| 370 |
m_output.AppendLine(String.format(" /* Code for method '%1$s' */", method.tokenText()));
|
|
| 371 |
DefineCadpAction(method, -1); |
|
| 372 |
} |
|
| 373 |
|
|
| 374 |
|
|
| 375 |
|
|
| 376 |
|
|
| 377 |
/// |
|
| 378 |
/// Dump Actions |
|
| 379 |
/// |
|
| 380 |
int actnum = 0; |
|
| 381 |
for (final NamedActionIdentifier action : actions) |
|
| 382 |
{
|
|
| 383 |
line(); |
|
| 384 |
m_output.AppendLine(String.format(" /* Code for action '%1$s' */", action.tokenText()));
|
|
| 385 |
DefineCadpAction(action, actnum); |
|
| 386 |
actnum++; |
|
| 387 |
} |
|
| 388 |
|
|
| 389 |
|
|
| 390 |
/// |
|
| 391 |
/// ITERATE STATE |
|
| 392 |
/// |
|
| 393 |
line(); |
|
| 394 |
line(); |
|
| 395 |
DefineCadpIterateState(ooActionSystemType); |
|
| 396 |
|
|
| 397 |
|
|
| 398 |
|
|
| 399 |
line(); |
|
| 400 |
m_output.AppendLine("void CAESAR_INIT_GRAPH ()");
|
|
| 401 |
lp(); |
|
| 402 |
m_output.AppendLine(" CAESAR_CHECK_VERSION (2.4, 2.4);");
|
|
| 403 |
rp(); |
|
| 404 |
m_output.AppendLine(); |
|
| 405 |
} |
|
| 406 |
|
|
| 407 |
@Override |
|
| 408 |
public void visit(MainModule mainModule) |
|
| 409 |
{
|
|
| 410 |
// define complex types |
|
| 411 |
DumpTypes(mainModule); |
|
| 412 |
|
|
| 413 |
// export action system |
|
| 414 |
Dump(mainModule.instance()); |
|
| 415 |
} |
|
| 416 |
|
|
| 417 |
|
|
| 418 |
|
|
| 419 |
|
|
| 420 |
// private String GetIdentifierString(TypeIdentifier typeIdentifier) |
|
| 421 |
// {
|
|
| 422 |
// return CadpIdentifier.GetIdentifierString(typeIdentifier); |
|
| 423 |
// } |
|
| 424 |
|
|
| 425 |
|
|
| 426 |
|
|
| 427 |
private void DumpTypes(MainModule mainModule) |
|
| 428 |
{
|
|
| 429 |
for (final Identifier x: mainModule.symbolTable().symbolList()) |
|
| 430 |
{
|
|
| 431 |
if (x.kind() == IdentifierKind.TypeIdentifier)/* && |
|
| 432 |
((TypeIdentifier)x).type.kind != TypeKind.OoActionSystemType)*/ |
|
| 433 |
{
|
|
| 434 |
final TypeIdentifier aTypeId = (TypeIdentifier)x; |
|
| 435 |
CadpType.EmitType(aTypeId.type()); |
|
| 436 |
} |
|
| 437 |
} |
|
| 438 |
} |
|
| 439 |
|
|
| 440 |
public OoaCADPVisitor(ParserState aState) |
|
| 441 |
{
|
|
| 442 |
super(aState); |
|
| 443 |
m_output = new OoasCodeEmitter(); |
|
| 444 |
m_statevector = new ArrayList<AttributeIdentifier>(); |
|
| 445 |
// m_AttributePre = ""; |
|
| 446 |
|
|
| 447 |
// clear helpers |
|
| 448 |
CadpExpression.emittedOperations.clear(); |
|
| 449 |
} |
|
| 450 |
|
|
| 451 |
|
|
| 452 |
@Override |
|
| 453 |
public String toString() |
|
| 454 |
{
|
|
| 455 |
final OoasCodeEmitter result = new OoasCodeEmitter(); |
|
| 456 |
DumpHeader(result); // comments, version |
|
| 457 |
DumpDefinitions(result); // includes, definitions |
|
| 458 |
|
|
| 459 |
result.AppendLine(CadpType.GetTypeDefintions()); |
|
| 460 |
result.AppendLine(cadpstate.toString()); |
|
| 461 |
result.AppendLine(CadpExpression.GetHelperCode()); |
|
| 462 |
result.AppendLine(m_output.toString()); |
|
| 463 |
|
|
| 464 |
return result.toString(); |
|
| 465 |
} |
|
| 466 |
|
|
| 467 |
|
|
| 468 |
|
|
| 469 |
|
|
| 470 |
|
|
| 471 |
|
|
| 472 |
private void line() |
|
| 473 |
{
|
|
| 474 |
m_output.AppendLine(); |
|
| 475 |
m_output.AppendLine("//----------------------------------------------------------------------");
|
|
| 476 |
} |
|
| 477 |
private void rp() |
|
| 478 |
{
|
|
| 479 |
m_output.AppendLine("}");
|
|
| 480 |
} |
|
| 481 |
private void lp() |
|
| 482 |
{
|
|
| 483 |
m_output.AppendLine("{");
|
|
| 484 |
} |
|
| 485 |
|
|
| 486 |
|
|
| 487 |
public static String DumpType(UlyssesType atype) |
|
| 488 |
{
|
|
| 489 |
final CadpType newtype = new CadpType(); |
|
| 490 |
atype.Accept(newtype); |
|
| 491 |
return newtype.ToString(); |
|
| 492 |
} |
|
| 493 |
|
|
| 494 |
|
|
| 495 |
/// <summary> |
|
| 496 |
/// Dumps a state variable (attribute) |
|
| 497 |
/// </summary> |
|
| 498 |
private void DumpAttribute(AttributeIdentifier attributeIdentifier) |
|
| 499 |
{
|
|
| 500 |
m_output.Append(DumpType(attributeIdentifier.type())); |
|
| 501 |
m_output.Append(" ");
|
|
| 502 |
m_output.Append(attributeIdentifier.tokenText()); |
|
| 503 |
m_statevector.add(attributeIdentifier); |
|
| 504 |
} |
|
| 505 |
|
|
| 506 |
private final OoasCodeEmitter cadpstate = new OoasCodeEmitter(); |
|
| 507 |
|
|
| 508 |
/// <summary> |
|
| 509 |
/// Exports the state of the ooActionSystem |
|
| 510 |
/// </summary> |
|
| 511 |
private void DefineCadpState(OoActionSystemType ooActionSystemType) |
|
| 512 |
{
|
|
| 513 |
final OoasCodeEmitter tmp = m_output; |
|
| 514 |
m_output = cadpstate; |
|
| 515 |
|
|
| 516 |
m_output.AppendLine("typedef struct CAESAR_STRUCT_STATE CAESAR_BODY_STATE;");
|
|
| 517 |
m_output.AppendLine("#ifdef WINDOWSPACK");
|
|
| 518 |
m_output.AppendLine("#pragma pack(1)");
|
|
| 519 |
m_output.AppendLine("#endif");
|
|
| 520 |
m_output.AppendLine("struct CAESAR_STRUCT_STATE {");
|
|
| 521 |
m_output.AppendLine("struct CAESAR_STRUCT_STATE *_predecessor;");
|
|
| 522 |
m_output.AppendLine("struct STATE_LIST *_successors;");
|
|
| 523 |
m_output.AppendLine("char *_statenum;");
|
|
| 524 |
m_output.AppendLine("char _hidden;");
|
|
| 525 |
for (final Identifier sym: ooActionSystemType.symbols().symbolList()) |
|
| 526 |
{
|
|
| 527 |
if (sym.kind() == IdentifierKind.AttributeIdentifier) |
|
| 528 |
{
|
|
| 529 |
DumpAttribute((AttributeIdentifier)sym); |
|
| 530 |
m_output.AppendLine(";");
|
|
| 531 |
} |
|
| 532 |
} |
|
| 533 |
m_output.AppendLine("} UNIXPACK;");
|
|
| 534 |
|
|
| 535 |
m_output = tmp; |
|
| 536 |
|
|
| 537 |
// now define the hash sizes, malloc and free routines, and aligned state |
|
| 538 |
m_output.AppendLine(); |
|
| 539 |
m_output.AppendLine("#undef CAESAR_SIZE_STATE");
|
|
| 540 |
m_output.AppendLine("#undef CAESAR_HASH_SIZE_STATE");
|
|
| 541 |
m_output.AppendLine("#undef CAESAR_CREATE_STATE");
|
|
| 542 |
m_output.AppendLine("#undef CAESAR_DELETE_STATE");
|
|
| 543 |
m_output.AppendLine("");
|
|
| 544 |
|
|
| 545 |
m_output.AppendLine(); |
|
| 546 |
m_output.AppendLine("#define CAESAR_SIZE_STATE() (sizeof (CAESAR_BODY_STATE))");
|
|
| 547 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_SIZE_STATE = CAESAR_SIZE_STATE();");
|
|
| 548 |
|
|
| 549 |
m_output.AppendLine(); |
|
| 550 |
m_output.AppendLine("#define CAESAR_HASH_SIZE_STATE() (CAESAR_SIZE_STATE ())");
|
|
| 551 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_HASH_SIZE_STATE = CAESAR_HASH_SIZE_STATE();");
|
|
| 552 |
|
|
| 553 |
m_output.AppendLine("#define CAESAR_CREATE_STATE(CAESAR_S)\\");
|
|
| 554 |
m_output.AppendLine(" { CAESAR_CREATE (*(CAESAR_S), CAESAR_SIZE_STATE(), CAESAR_TYPE_STATE); ((struct CAESAR_STRUCT_STATE*)(*(CAESAR_S)))->_hidden = 0; }");
|
|
| 555 |
|
|
| 556 |
m_output.AppendLine("");
|
|
| 557 |
m_output.AppendLine("#define CAESAR_DELETE_STATE(CAESAR_S)\\");
|
|
| 558 |
m_output.AppendLine(" { DELETE_STATES(((struct CAESAR_STRUCT_STATE*)*(CAESAR_S))->_successors); CAESAR_DELETE(*(CAESAR_S)); *(CAESAR_S) = NULL; }");
|
|
| 559 |
|
|
| 560 |
m_output.AppendLine(); |
|
| 561 |
m_output.AppendLine("typedef struct CAESAR_STRUCT_ALIGNMENT_STATE {");
|
|
| 562 |
m_output.AppendLine(" char CAESAR_BYTE;");
|
|
| 563 |
m_output.AppendLine(" CAESAR_BODY_STATE CAESAR_S;");
|
|
| 564 |
m_output.AppendLine("} CAESAR_BODY_ALIGNMENT_STATE;");
|
|
| 565 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_ALIGNMENT_STATE = sizeof (CAESAR_BODY_ALIGNMENT_STATE) - sizeof (CAESAR_BODY_STATE);");
|
|
| 566 |
|
|
| 567 |
line(); |
|
| 568 |
|
|
| 569 |
DefineCadpStateHelpers(ooActionSystemType); |
|
| 570 |
|
|
| 571 |
line(); |
|
| 572 |
} |
|
| 573 |
|
|
| 574 |
private void DefineCadpStateHelpers(OoActionSystemType ooActionSystemType) |
|
| 575 |
{
|
|
| 576 |
m_output.AppendLine("#include \"argos_runtime_helpers.c\"");
|
|
| 577 |
m_output.AppendLine("");
|
|
| 578 |
|
|
| 579 |
|
|
| 580 |
// final IScope ascope = ooActionSystemType.GetParentScope(); |
|
| 581 |
// final MainModule mainscope = (MainModule)ascope; |
|
| 582 |
|
|
| 583 |
} |
|
| 584 |
|
|
| 585 |
|
|
| 586 |
|
|
| 587 |
/// <summary> |
|
| 588 |
/// Exports a function that compares two states. |
|
| 589 |
/// </summary> |
|
| 590 |
private void DefineCompareCadpStates() |
|
| 591 |
{
|
|
| 592 |
m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_COMPARE_STATE (CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_STATE CAESAR_S2)");
|
|
| 593 |
lp(); |
|
| 594 |
m_output.AppendLine(" CAESAR_TYPE_BOOLEAN CAESAR_RESULT;");
|
|
| 595 |
m_output.AppendLine(" if ((char*)CAESAR_S1 == (char*)CAESAR_S2) return 1;");
|
|
| 596 |
m_output.AppendLine(" if (CAESAR_S1->_hidden != CAESAR_S2->_hidden)");
|
|
| 597 |
m_output.AppendLine(" return 0;");
|
|
| 598 |
m_output.AppendLine(" else if (CAESAR_S1->_hidden == 0)");
|
|
| 599 |
m_output.AppendLine(String.format(" CAESAR_RESULT = (memcmp (((char *) CAESAR_S1) + 3* %1$s, ((char *) CAESAR_S2)+3* %1$s , CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"/*, CadpType.sizeOfTypes["pointer"]*/));
|
|
| 600 |
m_output.AppendLine(" else");
|
|
| 601 |
m_output.AppendLine(" {");
|
|
| 602 |
m_output.AppendLine(String.format("/* CAESAR_RESULT = (memcmp (((char *) CAESAR_S1)+3* %1$s, ((char *) CAESAR_S2)+3* %1$s, CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"/*CadpType.sizeOfTypes["pointer"]*/));
|
|
| 603 |
m_output.AppendLine(" if (CAESAR_RESULT) {");
|
|
| 604 |
m_output.AppendLine(" char succequal;");
|
|
| 605 |
m_output.AppendLine(" COMPARE_STATES(CAESAR_S1->_successors,CAESAR_S2->_successors,succequal);");
|
|
| 606 |
m_output.AppendLine(" CAESAR_RESULT = CAESAR_RESULT && succequal;}*/");
|
|
| 607 |
m_output.AppendLine(" CAESAR_RESULT = 0;");
|
|
| 608 |
/*m_output.AppendLine("");
|
|
| 609 |
m_output.AppendLine(String.format(" CAESAR_RESULT = CAESAR_S1->_statenum == CAESAR_S2->_statenum && (memcmp (((char *) CAESAR_S1)+3* %1$s, ((char *) CAESAR_S2)+3* %1$s, CAESAR_HASH_SIZE_STATE ()-3*%1$s) == 0);", "sizeof(char*)"));*/
|
|
| 610 |
m_output.AppendLine(" }");
|
|
| 611 |
m_output.AppendLine(" return (CAESAR_RESULT);");
|
|
| 612 |
rp(); |
|
| 613 |
} |
|
| 614 |
|
|
| 615 |
/// <summary> |
|
| 616 |
/// Exports a hash function. Standard CADP implementation. |
|
| 617 |
/// </summary> |
|
| 618 |
private void DefineCadpStateHash() |
|
| 619 |
{
|
|
| 620 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HASH_STATE (CAESAR_TYPE_STATE CAESAR_ST, CAESAR_TYPE_NATURAL CAESAR_MODULUS)");
|
|
| 621 |
lp(); |
|
| 622 |
m_output.AppendLine(" /* we do not care about the pre/succ/... pointers here */");
|
|
| 623 |
m_output.AppendLine("int beg_offset = 3 * sizeof(unsigned char*);");
|
|
| 624 |
m_output.AppendLine(" CAESAR_TYPE_STATE CAESAR_S = (CAESAR_TYPE_STATE) ((unsigned char*)CAESAR_ST + beg_offset);");
|
|
| 625 |
m_output.AppendLine(" CAESAR_TYPE_NATURAL CAESAR_RESULT;");
|
|
| 626 |
m_output.AppendLine(" CAESAR_TYPE_WORD CAESAR_SHIFT_LOW, CAESAR_SHIFT_HIGH;");
|
|
| 627 |
m_output.AppendLine(" CAESAR_TYPE_WORD *CAESAR_LOW, *CAESAR_HIGH;");
|
|
| 628 |
m_output.AppendLine(" CAESAR_SHIFT_LOW = ((CAESAR_TYPE_WORD) CAESAR_S) % CAESAR_WORD_SIZE;");
|
|
| 629 |
m_output.AppendLine(" CAESAR_LOW = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_S - CAESAR_SHIFT_LOW);");
|
|
| 630 |
m_output.AppendLine(" CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_S + CAESAR_HASH_SIZE_STATE () - beg_offset);");
|
|
| 631 |
m_output.AppendLine(" CAESAR_SHIFT_HIGH = ((CAESAR_TYPE_WORD) CAESAR_HIGH) % CAESAR_WORD_SIZE;");
|
|
| 632 |
m_output.AppendLine(" CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_HIGH - CAESAR_SHIFT_HIGH);");
|
|
| 633 |
m_output.AppendLine(" if (CAESAR_LOW == CAESAR_HIGH) {");
|
|
| 634 |
m_output.AppendLine(" CAESAR_RESULT = htonl (*CAESAR_LOW);");
|
|
| 635 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW)");
|
|
| 636 |
m_output.AppendLine(" CAESAR_RESULT &= CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW);");
|
|
| 637 |
m_output.AppendLine(" if (CAESAR_SHIFT_HIGH)");
|
|
| 638 |
m_output.AppendLine(" CAESAR_RESULT &= CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH));");
|
|
| 639 |
m_output.AppendLine(" }");
|
|
| 640 |
m_output.AppendLine(" else");
|
|
| 641 |
m_output.AppendLine(" {");
|
|
| 642 |
m_output.AppendLine(" CAESAR_RESULT = 0;");
|
|
| 643 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW) {");
|
|
| 644 |
m_output.AppendLine(" CAESAR_RESULT = htonl (*(CAESAR_LOW++)) & (CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW));");
|
|
| 645 |
m_output.AppendLine(" }");
|
|
| 646 |
m_output.AppendLine(" while (CAESAR_LOW < CAESAR_HIGH) {");
|
|
| 647 |
m_output.AppendLine(" CAESAR_RESULT ^= htonl (*(CAESAR_LOW++));");
|
|
| 648 |
m_output.AppendLine(" }");
|
|
| 649 |
m_output.AppendLine(" if (CAESAR_SHIFT_HIGH) {");
|
|
| 650 |
m_output.AppendLine(" CAESAR_RESULT ^= htonl (*CAESAR_LOW) & (CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH)));");
|
|
| 651 |
m_output.AppendLine(" }");
|
|
| 652 |
m_output.AppendLine(" }");
|
|
| 653 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW) ");
|
|
| 654 |
m_output.AppendLine(" CAESAR_RESULT = ((CAESAR_RESULT >> ((CAESAR_WORD_SIZE - CAESAR_SHIFT_LOW) * 8)) | (CAESAR_RESULT << (CAESAR_SHIFT_LOW * 8)));");
|
|
| 655 |
m_output.AppendLine(" CAESAR_RESULT = CAESAR_RESULT % CAESAR_MODULUS;");
|
|
| 656 |
m_output.AppendLine(" return (CAESAR_RESULT);");
|
|
| 657 |
rp(); |
|
| 658 |
} |
|
| 659 |
|
|
| 660 |
/// <summary> |
|
| 661 |
/// Exports a function to print the state |
|
| 662 |
/// </summary> |
|
| 663 |
private void DefineCadpPrintState() |
|
| 664 |
{
|
|
| 665 |
m_output.AppendLine("void CAESAR_PRINT_STATE (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_STATE CAESAR_S)");
|
|
| 666 |
m_output.AppendLine("{");
|
|
| 667 |
m_output.AppendLine(" switch (CAESAR_CURRENT_STATE_FORMAT) {");
|
|
| 668 |
m_output.AppendLine(" case 0:");
|
|
| 669 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \"{\\n_hidden: %s,\\n\", CAESAR_S->_hidden == 0 ? \"0\": \"1\");");
|
|
| 670 |
int i = 0; |
|
| 671 |
for (final AttributeIdentifier x: m_statevector) |
|
| 672 |
{
|
|
| 673 |
CadpType.EmitType(x.type()); |
|
| 674 |
if (i != 0) |
|
| 675 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \",\\n\");");
|
|
| 676 |
|
|
| 677 |
i++; |
|
| 678 |
m_output.AppendLine(String.format(" fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
|
|
| 679 |
m_output.AppendLine(String.format(" %1$s%2$s(CAESAR_FILE, CAESAR_S->%3$s);", CadpType.printString,
|
|
| 680 |
CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText())); |
|
| 681 |
} |
|
| 682 |
m_output.Append(" fprintf (CAESAR_FILE, \"\\n}\");");
|
|
| 683 |
m_output.AppendLine(" break;");
|
|
| 684 |
m_output.AppendLine(" default:");
|
|
| 685 |
m_output.AppendLine(" {");
|
|
| 686 |
m_output.AppendLine(" printf(\"#233 bug during simulation:\\n unknown state printing format\\n\");");
|
|
| 687 |
m_output.AppendLine(" }");
|
|
| 688 |
m_output.AppendLine(" break;");
|
|
| 689 |
m_output.AppendLine(" }");
|
|
| 690 |
m_output.AppendLine("}");
|
|
| 691 |
} |
|
| 692 |
|
|
| 693 |
/// <summary> |
|
| 694 |
/// Exports a function to print the delta state.. |
|
| 695 |
/// </summary> |
|
| 696 |
private void DefineCadpPrintDeltaState() |
|
| 697 |
{
|
|
| 698 |
m_output.AppendLine("void CAESAR_DELTA_STATE (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_STATE CAESAR_S2)");
|
|
| 699 |
m_output.AppendLine("{");
|
|
| 700 |
m_output.AppendLine(" switch (CAESAR_CURRENT_STATE_FORMAT) {");
|
|
| 701 |
m_output.AppendLine(" case 0:");
|
|
| 702 |
|
|
| 703 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \"{_hidden: %s, \", CAESAR_S1->_hidden == 0 ? \"0\": \"1\");");
|
|
| 704 |
int i = 0; |
|
| 705 |
for (final AttributeIdentifier x: m_statevector) |
|
| 706 |
{
|
|
| 707 |
if (i != 0) |
|
| 708 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \", \");");
|
|
| 709 |
|
|
| 710 |
i++; |
|
| 711 |
m_output.AppendLine(String.format(" fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
|
|
| 712 |
m_output.AppendLine(String.format(" %1$s%2$s(CAESAR_FILE, CAESAR_S1->%3$s);", CadpType.printString,
|
|
| 713 |
CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText())); |
|
| 714 |
} |
|
| 715 |
m_output.Append(" fprintf (CAESAR_FILE, \"}\");");
|
|
| 716 |
|
|
| 717 |
|
|
| 718 |
|
|
| 719 |
m_output.Append(" fprintf (CAESAR_FILE, \" --->> \");");
|
|
| 720 |
|
|
| 721 |
|
|
| 722 |
|
|
| 723 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \"{_hidden: %s, \", CAESAR_S2->_hidden == 0 ? \"0\": \"1\");");
|
|
| 724 |
i = 0; |
|
| 725 |
for (final AttributeIdentifier x: m_statevector) |
|
| 726 |
{
|
|
| 727 |
if (i != 0) |
|
| 728 |
m_output.AppendLine(" fprintf (CAESAR_FILE, \", \");");
|
|
| 729 |
|
|
| 730 |
i++; |
|
| 731 |
m_output.AppendLine(String.format(" fprintf (CAESAR_FILE, \"%1$s: \");", x.tokenText()));
|
|
| 732 |
m_output.AppendLine(String.format(" %1$s%2$s(CAESAR_FILE, CAESAR_S2->%3$s);", CadpType.printString,
|
|
| 733 |
CadpIdentifier.GetIdentifierString(x.type().identifier()), x.tokenText())); |
|
| 734 |
} |
|
| 735 |
m_output.Append(" fprintf (CAESAR_FILE, \"}\");");
|
|
| 736 |
|
|
| 737 |
|
|
| 738 |
m_output.AppendLine(" break;");
|
|
| 739 |
m_output.AppendLine(" default:");
|
|
| 740 |
m_output.AppendLine(" {");
|
|
| 741 |
m_output.AppendLine(" printf(\"#233 bug during simulation:\\n unknown state printing format\\n\");");
|
|
| 742 |
m_output.AppendLine(" }");
|
|
| 743 |
m_output.AppendLine(" break;");
|
|
| 744 |
m_output.AppendLine(" }");
|
|
| 745 |
m_output.AppendLine("}");
|
|
| 746 |
} |
|
| 747 |
|
|
| 748 |
/// <summary> |
|
| 749 |
/// Defines CADP label data type and helper information |
|
| 750 |
/// </summary> |
|
| 751 |
private void DefineCadpLabel(OoActionSystemType ooActionSystemType) |
|
| 752 |
{
|
|
| 753 |
m_output.AppendLine("typedef unsigned int CAESAR_TYPE_PACKED_TRANSITION_NUMBER;");
|
|
| 754 |
m_output.AppendLine("typedef unsigned char CAESAR_TYPE_UNIQUE_GATE_AND_PROFILE_NUMBER;");
|
|
| 755 |
|
|
| 756 |
m_output.AppendLine("typedef struct CAESAR_STRUCT_LABEL {");
|
|
| 757 |
m_output.AppendLine(" CAESAR_TYPE_PACKED_TRANSITION_NUMBER CAESAR_TRANSITION_NUMBER;");
|
|
| 758 |
|
|
| 759 |
int i = 0; |
|
| 760 |
final StringBuilder param = new StringBuilder(); |
|
| 761 |
for (final Identifier sym: ooActionSystemType.symbols().symbolList()) |
|
| 762 |
{
|
|
| 763 |
if (sym.kind() == IdentifierKind.NamedActionIdentifier) |
|
| 764 |
{
|
|
| 765 |
final NamedActionIdentifier namedAction = (NamedActionIdentifier)sym; |
|
| 766 |
|
|
| 767 |
if (((FunctionType)namedAction.type()).parameter().size() > 0) |
|
| 768 |
{
|
|
| 769 |
param.append(" struct {"); param.append(System.lineSeparator());
|
|
| 770 |
int parnum = 0; |
|
| 771 |
for (final UlyssesType parameter: ((FunctionType)namedAction.type()).parameter()) |
|
| 772 |
{
|
|
| 773 |
param.append(String.format(" %1$s PARAM_%2$s;", DumpType(parameter), parnum));
|
|
| 774 |
param.append(System.lineSeparator()); |
|
| 775 |
parnum++; |
|
| 776 |
} |
|
| 777 |
param.append(String.format(" } CAESAR_PROFILE_%1$s;", i));
|
|
| 778 |
param.append(System.lineSeparator()); |
|
| 779 |
} |
|
| 780 |
actions.add(namedAction); |
|
| 781 |
i++; |
|
| 782 |
} |
|
| 783 |
else if (sym.kind() == IdentifierKind.MethodIdentifier) |
|
| 784 |
{
|
|
| 785 |
methods.add((MethodIdentifier)sym); |
|
| 786 |
} |
|
| 787 |
} |
|
| 788 |
m_output.AppendLine(" union {");
|
|
| 789 |
if (param.length() > 0) |
|
| 790 |
m_output.Append(param.toString()); |
|
| 791 |
m_output.AppendLine(" } CAESAR_UNION;");
|
|
| 792 |
m_output.AppendLine("} CAESAR_BODY_LABEL;");
|
|
| 793 |
m_output.AppendLine(); |
|
| 794 |
m_internalActionNumber = actions.size(); |
|
| 795 |
|
|
| 796 |
m_output.AppendLine(String.format("#define INTERNAL_ACTION_NUMBER %1$s", m_internalActionNumber));
|
|
| 797 |
m_output.AppendLine("#define INTERNAL_ACTION 0");
|
|
| 798 |
m_output.AppendLine("#define OBSERVABLE_ACTION 1");
|
|
| 799 |
m_output.AppendLine("#define CONTROLLABLE_ACTION 2");
|
|
| 800 |
|
|
| 801 |
final StringBuilder gatelist = new StringBuilder(String.format("CAESAR_TYPE_STRING CAESAR_GATE[%1$s] = {", (actions.size() + 1)));
|
|
| 802 |
final StringBuilder cardlist = new StringBuilder(String.format("CAESAR_TYPE_NATURAL CAESAR_CARDINAL[%1$s] = {", (actions.size() + 1)));
|
|
| 803 |
final StringBuilder intObsCtrList = new StringBuilder(String.format("CAESAR_TYPE_NATURAL CAESAR_GATEKIND[%1$s] = {", (actions.size() + 1)));
|
|
| 804 |
int j = 0; |
|
| 805 |
for (final NamedActionIdentifier action: actions) |
|
| 806 |
{
|
|
| 807 |
if (j != 0) |
|
| 808 |
{
|
|
| 809 |
gatelist.append(", ");
|
|
| 810 |
cardlist.append(", ");
|
|
| 811 |
intObsCtrList.append(", ");
|
|
| 812 |
} |
|
| 813 |
j++; |
|
| 814 |
gatelist.append(String.format("\"%1$s\"", action.tokenText()));
|
|
| 815 |
cardlist.append(((FunctionType)action.type()).parameter().size()); |
|
| 816 |
if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Observable) |
|
| 817 |
intObsCtrList.append("OBSERVABLE_ACTION");
|
|
| 818 |
else if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Controllable) |
|
| 819 |
intObsCtrList.append("CONTROLLABLE_ACTION");
|
|
| 820 |
else |
|
| 821 |
intObsCtrList.append("INTERNAL_ACTION");
|
|
| 822 |
} |
|
| 823 |
gatelist.append(",\"i\"};");
|
|
| 824 |
cardlist.append(",0};");
|
|
| 825 |
intObsCtrList.append(",INTERNAL_ACTION};");
|
|
| 826 |
|
|
| 827 |
m_output.AppendLine("/* Names of actions (= gates) */");
|
|
| 828 |
m_output.AppendLine(gatelist.toString()); |
|
| 829 |
m_output.AppendLine("/* Number of parameters of actions (= cardinality) */");
|
|
| 830 |
m_output.AppendLine(cardlist.toString()); |
|
| 831 |
m_output.AppendLine("/* Internal (0), Observable (1), or Controllable (2) action? */");
|
|
| 832 |
m_output.AppendLine(intObsCtrList.toString()); |
|
| 833 |
|
|
| 834 |
m_output.AppendLine("#undef CAESAR_SIZE_LABEL");
|
|
| 835 |
m_output.AppendLine("#define CAESAR_SIZE_LABEL() (sizeof (CAESAR_BODY_LABEL))");
|
|
| 836 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_SIZE_LABEL = CAESAR_SIZE_LABEL();");
|
|
| 837 |
m_output.AppendLine("#undef CAESAR_HASH_SIZE_LABEL");
|
|
| 838 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HINT_HASH_SIZE_LABEL;");
|
|
| 839 |
m_output.AppendLine("#define CAESAR_HASH_SIZE_LABEL() CAESAR_HINT_HASH_SIZE_LABEL");
|
|
| 840 |
} |
|
| 841 |
|
|
| 842 |
/// <summary> |
|
| 843 |
/// Method that exports the CAESAR_STRING_LABEL function |
|
| 844 |
/// </summary> |
|
| 845 |
private void DefineCadpGetStringLabel() |
|
| 846 |
{
|
|
| 847 |
|
|
| 848 |
m_output.AppendLine("CAESAR_TYPE_FILE CAESAR_BUFFER = NULL;");
|
|
| 849 |
m_output.AppendLine("");
|
|
| 850 |
m_output.AppendLine("CAESAR_TYPE_STRING CAESAR_STRING_LABEL (CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 851 |
lp(); |
|
| 852 |
|
|
| 853 |
m_output.AppendLine(" CAESAR_TYPE_STRING CAESAR_RESULT;");
|
|
| 854 |
m_output.AppendLine("");
|
|
| 855 |
m_output.AppendLine(" #define CAESAR_LABEL_HASH_SIZE 10007");
|
|
| 856 |
m_output.AppendLine(" typedef struct CAESAR_STRUCT_LABEL_STRING {");
|
|
| 857 |
m_output.AppendLine(" CAESAR_BODY_LABEL CAESAR_LABEL;");
|
|
| 858 |
m_output.AppendLine(" CAESAR_TYPE_STRING CAESAR_STRING;");
|
|
| 859 |
m_output.AppendLine(" } CAESAR_BODY_LABEL_STRING, *CAESAR_TYPE_LABEL_STRING;");
|
|
| 860 |
m_output.AppendLine(" static CAESAR_TYPE_LABEL_STRING CAESAR_LABEL_STRING_TABLE = NULL;");
|
|
| 861 |
m_output.AppendLine(" /*static CAESAR_TYPE_FILE CAESAR_BUFFER = NULL;*/");
|
|
| 862 |
m_output.AppendLine(" CAESAR_TYPE_NATURAL CAESAR_N;");
|
|
| 863 |
m_output.AppendLine(" CAESAR_TYPE_LABEL_STRING CAESAR_ITEM;");
|
|
| 864 |
m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
|
|
| 865 |
m_output.AppendLine(" static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_HIT = 0;");
|
|
| 866 |
m_output.AppendLine(" static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_MISS = 0;");
|
|
| 867 |
m_output.AppendLine(" static CAESAR_TYPE_NATURAL CAESAR_LABEL_STRING_TABLE_CONFLICT = 0;");
|
|
| 868 |
m_output.AppendLine("#endif");
|
|
| 869 |
m_output.AppendLine("");
|
|
| 870 |
|
|
| 871 |
m_output.AppendLine(" /* If action has no params, then label is name of action */");
|
|
| 872 |
m_output.AppendLine(" //if (CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER] == 0)");
|
|
| 873 |
m_output.AppendLine(" // CAESAR_RESULT = CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER];");
|
|
| 874 |
m_output.AppendLine(" //else");
|
|
| 875 |
m_output.AppendLine(" {");
|
|
| 876 |
m_output.AppendLine(" /* otherwise.. (standard CADP) */");
|
|
| 877 |
|
|
| 878 |
m_output.AppendLine(" if (CAESAR_LABEL_STRING_TABLE == NULL) {");
|
|
| 879 |
m_output.AppendLine(" CAESAR_CREATE (CAESAR_LABEL_STRING_TABLE, CAESAR_LABEL_HASH_SIZE * sizeof (CAESAR_BODY_LABEL_STRING), CAESAR_TYPE_LABEL_STRING);");
|
|
| 880 |
m_output.AppendLine(" if (CAESAR_LABEL_STRING_TABLE == NULL)");
|
|
| 881 |
m_output.AppendLine(" {");
|
|
| 882 |
m_output.AppendLine(" printf(\"#211 bug during simulation:\\n out of memory when allocating string table\\n\");");
|
|
| 883 |
m_output.AppendLine(" printf(\" abandon\\n\");");
|
|
| 884 |
m_output.AppendLine(" CAESAR_TERMINATE (1);");
|
|
| 885 |
m_output.AppendLine(" exit(1);");
|
|
| 886 |
m_output.AppendLine(" }");
|
|
| 887 |
m_output.AppendLine(" for (CAESAR_N = 0; CAESAR_N < CAESAR_LABEL_HASH_SIZE; CAESAR_N++)");
|
|
| 888 |
m_output.AppendLine(" CAESAR_LABEL_STRING_TABLE [CAESAR_N].CAESAR_STRING = NULL;");
|
|
| 889 |
m_output.AppendLine(" }");
|
|
| 890 |
m_output.AppendLine(" CAESAR_ITEM = CAESAR_LABEL_STRING_TABLE + CAESAR_HASH_LABEL (CAESAR_L, CAESAR_LABEL_HASH_SIZE);");
|
|
| 891 |
m_output.AppendLine(" if ((CAESAR_ITEM->CAESAR_STRING != NULL) && CAESAR_COMPARE_LABEL (&(CAESAR_ITEM->CAESAR_LABEL), CAESAR_L)) {");
|
|
| 892 |
m_output.AppendLine(" CAESAR_RESULT = CAESAR_ITEM->CAESAR_STRING;");
|
|
| 893 |
m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
|
|
| 894 |
m_output.AppendLine(" CAESAR_LABEL_STRING_TABLE_HIT++;");
|
|
| 895 |
m_output.AppendLine("#endif");
|
|
| 896 |
m_output.AppendLine(" } else {");
|
|
| 897 |
m_output.AppendLine(" if (CAESAR_ITEM->CAESAR_STRING == NULL) {");
|
|
| 898 |
m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
|
|
| 899 |
m_output.AppendLine(" CAESAR_LABEL_STRING_TABLE_MISS++;");
|
|
| 900 |
m_output.AppendLine("#endif");
|
|
| 901 |
m_output.AppendLine(" } else {");
|
|
| 902 |
m_output.AppendLine(" CAESAR_DELETE (CAESAR_ITEM->CAESAR_STRING);");
|
|
| 903 |
m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
|
|
| 904 |
m_output.AppendLine(" CAESAR_LABEL_STRING_TABLE_CONFLICT++;");
|
|
| 905 |
m_output.AppendLine("#endif");
|
|
| 906 |
m_output.AppendLine(" }");
|
|
| 907 |
m_output.AppendLine(" CAESAR_ITEM->CAESAR_LABEL = *CAESAR_L;");
|
|
| 908 |
m_output.AppendLine(" if (CAESAR_BUFFER == NULL) {");
|
|
| 909 |
m_output.AppendLine(" CAESAR_BUFFER = (CAESAR_TYPE_FILE) tmpfile ();");
|
|
| 910 |
m_output.AppendLine(" if (CAESAR_BUFFER == NULL)");
|
|
| 911 |
m_output.AppendLine(" {");
|
|
| 912 |
m_output.AppendLine(" printf(\"#212 bug during simulation :\\n cannot allocate tmpfile\\n\");");
|
|
| 913 |
m_output.AppendLine(" printf(\" aborting.\\n\");");
|
|
| 914 |
m_output.AppendLine(" CAESAR_TERMINATE (1);");
|
|
| 915 |
m_output.AppendLine(" exit(1);");
|
|
| 916 |
m_output.AppendLine(" }");
|
|
| 917 |
m_output.AppendLine(" }");
|
|
| 918 |
m_output.AppendLine(" CAESAR_PRINT_LABEL (CAESAR_BUFFER, CAESAR_L);");
|
|
| 919 |
m_output.AppendLine(" CAESAR_N = ftell (CAESAR_BUFFER) + 1;");
|
|
| 920 |
m_output.AppendLine(" rewind (CAESAR_BUFFER);");
|
|
| 921 |
m_output.AppendLine(" CAESAR_CREATE (CAESAR_ITEM->CAESAR_STRING, CAESAR_N, CAESAR_TYPE_STRING);");
|
|
| 922 |
m_output.AppendLine(" if (CAESAR_ITEM->CAESAR_STRING == NULL)");
|
|
| 923 |
m_output.AppendLine(" {");
|
|
| 924 |
m_output.AppendLine(" printf(\"#213 bug during simulation :\\n out of memory\\n\");");
|
|
| 925 |
m_output.AppendLine(" printf(\" aborting\\n\");");
|
|
| 926 |
m_output.AppendLine(" CAESAR_TERMINATE (1);");
|
|
| 927 |
m_output.AppendLine(" exit(1);");
|
|
| 928 |
m_output.AppendLine(" }");
|
|
| 929 |
m_output.AppendLine(" if (fgets (CAESAR_ITEM->CAESAR_STRING, CAESAR_N, CAESAR_BUFFER) == NULL)");
|
|
| 930 |
m_output.AppendLine(" {");
|
|
| 931 |
m_output.AppendLine(" printf(\"#214 bug during simulation :\\n fgets \\n\");");
|
|
| 932 |
m_output.AppendLine(" printf(\" aborting.\\n\");");
|
|
| 933 |
m_output.AppendLine(" CAESAR_TERMINATE (1);");
|
|
| 934 |
m_output.AppendLine(" exit(1);");
|
|
| 935 |
m_output.AppendLine(" }");
|
|
| 936 |
m_output.AppendLine(" rewind (CAESAR_BUFFER);");
|
|
| 937 |
m_output.AppendLine(" CAESAR_RESULT = CAESAR_ITEM->CAESAR_STRING;");
|
|
| 938 |
m_output.AppendLine(" }");
|
|
| 939 |
m_output.AppendLine(" }");
|
|
| 940 |
m_output.AppendLine("#ifdef CAESAR_LABEL_STRING_STATISTICS");
|
|
| 941 |
m_output.AppendLine(" fprintf (stderr, \"label table statistics: hit=%u miss=%u conflict=%u total=%u\\n\", CAESAR_LABEL_STRING_TABLE_HIT, CAESAR_LABEL_STRING_TABLE_MISS, CAESAR_LABEL_STRING_TABLE_CONFLICT, CAESAR_LABEL_STRING_TABLE_HIT + CAESAR_LABEL_STRING_TABLE_MISS+CAESAR_LABEL_STRING_TABLE_CONFLICT);");
|
|
| 942 |
m_output.AppendLine("#endif");
|
|
| 943 |
m_output.AppendLine(" return CAESAR_RESULT;");
|
|
| 944 |
rp(); |
|
| 945 |
} |
|
| 946 |
|
|
| 947 |
/// <summary> |
|
| 948 |
/// Method that exports the CAESAR_COMPARE_LABEL function |
|
| 949 |
/// </summary> |
|
| 950 |
private void DefineCadpCompareLabel() |
|
| 951 |
{
|
|
| 952 |
m_output.AppendLine("CAESAR_TYPE_BOOLEAN CAESAR_COMPARE_LABEL (CAESAR_TYPE_LABEL CAESAR_L1, CAESAR_TYPE_LABEL CAESAR_L2)");
|
|
| 953 |
lp(); |
|
| 954 |
m_output.AppendLine(" CAESAR_TYPE_PACKED_TRANSITION_NUMBER CAESAR_N1, CAESAR_N2;");
|
|
| 955 |
m_output.AppendLine(" CAESAR_N1 = CAESAR_L1->CAESAR_TRANSITION_NUMBER;");
|
|
| 956 |
m_output.AppendLine(" CAESAR_N2 = CAESAR_L2->CAESAR_TRANSITION_NUMBER;");
|
|
| 957 |
m_output.AppendLine("");
|
|
| 958 |
m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
|
|
| 959 |
m_output.AppendLine("if (CAESAR_GATEKIND[CAESAR_N1] == INTERNAL_ACTION && CAESAR_GATEKIND[CAESAR_N2] == INTERNAL_ACTION)");
|
|
| 960 |
m_output.AppendLine(" return 1;");
|
|
| 961 |
m_output.AppendLine("#endif");
|
|
| 962 |
m_output.AppendLine("");
|
|
| 963 |
m_output.AppendLine(" /* if the labels encode different actions, then they are different.. */");
|
|
| 964 |
m_output.AppendLine(" if (CAESAR_N1 != CAESAR_N2)");
|
|
| 965 |
m_output.AppendLine(" return 0;");
|
|
| 966 |
m_output.AppendLine(" /* if it is the same action, then compare the parameters */ ");
|
|
| 967 |
m_output.AppendLine(" if (CAESAR_CARDINAL[CAESAR_N1] == 0)");
|
|
| 968 |
m_output.AppendLine(" return 1; /*no params, hence the same*/");
|
|
| 969 |
m_output.AppendLine(" switch(CAESAR_N1)");
|
|
| 970 |
m_output.AppendLine(" {");
|
|
| 971 |
|
|
| 972 |
int num = 0; |
|
| 973 |
for (final NamedActionIdentifier action: actions) |
|
| 974 |
{
|
|
| 975 |
if (((FunctionType)action.type()).parameter().size() > 0) |
|
| 976 |
{
|
|
| 977 |
m_output.AppendLine(String.format(" case %1$s:", num));
|
|
| 978 |
m_output.Append(" return ");
|
|
| 979 |
int paramnr = 0; |
|
| 980 |
for (final UlyssesType param: ((FunctionType)action.type()).parameter()) |
|
| 981 |
{
|
|
| 982 |
if (paramnr != 0) |
|
| 983 |
m_output.AppendLine(" && ");
|
|
| 984 |
if (CadpType.IsNumeric(param)) |
|
| 985 |
|
|
| 986 |
m_output.Append( |
|
| 987 |
String.format("CAESAR_L1->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s == CAESAR_L2->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s", num, paramnr));
|
|
| 988 |
else |
|
| 989 |
m_output.Append( |
|
| 990 |
String.format("0 == memcmp(&(CAESAR_L1->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s),&(CAESAR_L2->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s),sizeof(%3$s))", num, paramnr, CadpType.DumpType(param)));
|
|
| 991 |
|
|
| 992 |
paramnr++; |
|
| 993 |
} |
|
| 994 |
m_output.AppendLine(";");
|
|
| 995 |
} |
|
| 996 |
num++; |
|
| 997 |
} |
|
| 998 |
m_output.AppendLine(" }");
|
|
| 999 |
m_output.AppendLine(" printf(\"#211 bug during simulation :\\n CAESAR_COMPARE_LABEL\\n\");");
|
|
| 1000 |
m_output.AppendLine(" printf(\" aborting\\n\");");
|
|
| 1001 |
m_output.AppendLine(" CAESAR_TERMINATE (1);");
|
|
| 1002 |
m_output.AppendLine(" exit(1);");
|
|
| 1003 |
rp(); |
|
| 1004 |
} |
|
| 1005 |
|
|
| 1006 |
/// <summary> |
|
| 1007 |
/// Method that exports the CAESAR_HASH_LABEL function |
|
| 1008 |
/// </summary> |
|
| 1009 |
private void DefineCadpHashLabel() |
|
| 1010 |
{
|
|
| 1011 |
m_output.AppendLine("CAESAR_TYPE_NATURAL CAESAR_HASH_LABEL (CAESAR_TYPE_LABEL CAESAR_L, CAESAR_TYPE_NATURAL CAESAR_MODULUS)");
|
|
| 1012 |
lp(); |
|
| 1013 |
m_output.AppendLine(" CAESAR_TYPE_NATURAL CAESAR_RESULT;");
|
|
| 1014 |
m_output.AppendLine(" CAESAR_TYPE_NATURAL CAESAR_SIZE;");
|
|
| 1015 |
m_output.AppendLine("");
|
|
| 1016 |
m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
|
|
| 1017 |
m_output.AppendLine(" if (CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION)");
|
|
| 1018 |
m_output.AppendLine(" return INTERNAL_ACTION_NUMBER % CAESAR_MODULUS;");
|
|
| 1019 |
m_output.AppendLine("#endif");
|
|
| 1020 |
m_output.AppendLine("");
|
|
| 1021 |
m_output.AppendLine(" /* if action has no params, then hash is trans num */");
|
|
| 1022 |
m_output.AppendLine(" if (CAESAR_CARDINAL[CAESAR_L->CAESAR_TRANSITION_NUMBER] == 0)");
|
|
| 1023 |
m_output.AppendLine(" return CAESAR_L->CAESAR_TRANSITION_NUMBER % CAESAR_MODULUS;");
|
|
| 1024 |
m_output.AppendLine(" /* otherwise it gets more complicated.. */");
|
|
| 1025 |
m_output.AppendLine(" switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
|
|
| 1026 |
m_output.AppendLine(" {");
|
|
| 1027 |
|
|
| 1028 |
int num = 0; |
|
| 1029 |
for (final NamedActionIdentifier action : actions) |
|
| 1030 |
{
|
|
| 1031 |
if (((FunctionType)action.type()).parameter().size() > 0) |
|
| 1032 |
{
|
|
| 1033 |
m_output.AppendLine(String.format(" case %1$s:", num));
|
|
| 1034 |
// int paramnr = 0; |
|
| 1035 |
for (@SuppressWarnings("unused") final UlyssesType param: ((FunctionType)action.type()).parameter())
|
|
| 1036 |
{
|
|
| 1037 |
m_output.AppendLine( |
|
| 1038 |
String.format(" CAESAR_SIZE = sizeof (CAESAR_L->CAESAR_UNION.CAESAR_PROFILE_%1$s);", num));
|
|
| 1039 |
m_output.AppendLine(" break;");
|
|
| 1040 |
// paramnr++; |
|
| 1041 |
} |
|
| 1042 |
} |
|
| 1043 |
num++; |
|
| 1044 |
} |
|
| 1045 |
m_output.AppendLine(" default:");
|
|
| 1046 |
m_output.AppendLine(" return CAESAR_L->CAESAR_TRANSITION_NUMBER % CAESAR_MODULUS;");
|
|
| 1047 |
m_output.AppendLine(" }");
|
|
| 1048 |
m_output.AppendLine(" {");
|
|
| 1049 |
m_output.AppendLine(" CAESAR_TYPE_WORD CAESAR_SHIFT_LOW, CAESAR_SHIFT_HIGH;");
|
|
| 1050 |
m_output.AppendLine(" CAESAR_TYPE_WORD *CAESAR_LOW, *CAESAR_HIGH;");
|
|
| 1051 |
m_output.AppendLine(" CAESAR_SHIFT_LOW = ((CAESAR_TYPE_WORD) (&(CAESAR_L->CAESAR_UNION))) % CAESAR_WORD_SIZE;");
|
|
| 1052 |
m_output.AppendLine(" CAESAR_LOW = (CAESAR_TYPE_WORD *) ((unsigned char *) (&(CAESAR_L->CAESAR_UNION)) - CAESAR_SHIFT_LOW);");
|
|
| 1053 |
m_output.AppendLine(" CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) (&(CAESAR_L->CAESAR_UNION)) + CAESAR_SIZE);");
|
|
| 1054 |
m_output.AppendLine(" CAESAR_SHIFT_HIGH = ((CAESAR_TYPE_WORD) CAESAR_HIGH) % CAESAR_WORD_SIZE;");
|
|
| 1055 |
m_output.AppendLine(" CAESAR_HIGH = (CAESAR_TYPE_WORD *) ((unsigned char *) CAESAR_HIGH - CAESAR_SHIFT_HIGH);");
|
|
| 1056 |
m_output.AppendLine(" if (CAESAR_LOW == CAESAR_HIGH) {");
|
|
| 1057 |
m_output.AppendLine(" CAESAR_RESULT = htonl (*CAESAR_LOW);");
|
|
| 1058 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW)");
|
|
| 1059 |
m_output.AppendLine(" CAESAR_RESULT &= CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW);");
|
|
| 1060 |
m_output.AppendLine(" if (CAESAR_SHIFT_HIGH)");
|
|
| 1061 |
m_output.AppendLine(" CAESAR_RESULT &= CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH));");
|
|
| 1062 |
m_output.AppendLine(" } else {");
|
|
| 1063 |
m_output.AppendLine(" CAESAR_RESULT = 0;");
|
|
| 1064 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW) {");
|
|
| 1065 |
m_output.AppendLine(" CAESAR_RESULT ^= htonl (*(CAESAR_LOW++)) & (CAESAR_FULL_MASK >> (8 * CAESAR_SHIFT_LOW));");
|
|
| 1066 |
m_output.AppendLine(" }");
|
|
| 1067 |
m_output.AppendLine(" while (CAESAR_LOW < CAESAR_HIGH) {");
|
|
| 1068 |
m_output.AppendLine(" CAESAR_RESULT ^= htonl (*(CAESAR_LOW++));");
|
|
| 1069 |
m_output.AppendLine(" }");
|
|
| 1070 |
m_output.AppendLine(" if (CAESAR_SHIFT_HIGH) {");
|
|
| 1071 |
m_output.AppendLine(" CAESAR_RESULT ^= htonl (*CAESAR_LOW) & (CAESAR_FULL_MASK << (8 * (CAESAR_WORD_SIZE - CAESAR_SHIFT_HIGH)));");
|
|
| 1072 |
m_output.AppendLine(" }");
|
|
| 1073 |
m_output.AppendLine(" }");
|
|
| 1074 |
m_output.AppendLine(" if (CAESAR_SHIFT_LOW) {");
|
|
| 1075 |
m_output.AppendLine(" CAESAR_RESULT = ((CAESAR_RESULT >> ((CAESAR_WORD_SIZE - CAESAR_SHIFT_LOW) * 8)) | (CAESAR_RESULT << (CAESAR_SHIFT_LOW * 8)));");
|
|
| 1076 |
m_output.AppendLine(" }");
|
|
| 1077 |
m_output.AppendLine(" CAESAR_RESULT = (CAESAR_RESULT ^ CAESAR_L->CAESAR_TRANSITION_NUMBER) % CAESAR_MODULUS;");
|
|
| 1078 |
m_output.AppendLine(" }");
|
|
| 1079 |
m_output.AppendLine(" return (CAESAR_RESULT);");
|
|
| 1080 |
rp(); |
|
| 1081 |
} |
|
| 1082 |
|
|
| 1083 |
/// <summary> |
|
| 1084 |
/// Method that exports the CAESAR_PRINT_LABEL function |
|
| 1085 |
/// </summary> |
|
| 1086 |
private void DefineCadpPrintLabel() |
|
| 1087 |
{
|
|
| 1088 |
m_output.AppendLine("void CAESAR_PRINT_LABEL (CAESAR_TYPE_FILE CAESAR_FILE, CAESAR_TYPE_LABEL CAESAR_L)");
|
|
| 1089 |
lp(); |
|
| 1090 |
|
|
| 1091 |
m_output.AppendLine(" char* actionTag = \"\";");
|
|
| 1092 |
m_output.AppendLine(" switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
|
|
| 1093 |
m_output.AppendLine(" {");
|
|
| 1094 |
int gatenum = 0; |
|
| 1095 |
for (final NamedActionIdentifier action: actions) |
|
| 1096 |
{
|
|
| 1097 |
m_output.AppendLine(String.format(" case %1$s:", gatenum));
|
|
| 1098 |
String controbsmark = ""; |
|
| 1099 |
if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Controllable) |
|
| 1100 |
controbsmark = "ctr "; |
|
| 1101 |
else if (((FunctionType)action.type()).functionType() == FunctionTypeEnum.Observable) |
|
| 1102 |
controbsmark = "obs "; |
|
| 1103 |
m_output.AppendLine(String.format(" actionTag = \"%1$s\";", controbsmark));
|
|
| 1104 |
m_output.AppendLine("break;");
|
|
| 1105 |
gatenum++; |
|
| 1106 |
} |
|
| 1107 |
m_output.AppendLine(" }");
|
|
| 1108 |
|
|
| 1109 |
m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
|
|
| 1110 |
m_output.AppendLine(" fprintf(CAESAR_FILE, \"%s%s\", actionTag, CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] == INTERNAL_ACTION ? CAESAR_GATE[INTERNAL_ACTION_NUMBER] : CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER]);");
|
|
| 1111 |
m_output.AppendLine("#else");
|
|
| 1112 |
m_output.AppendLine(" fprintf(CAESAR_FILE, \"%s%s\", actionTag, CAESAR_GATE[CAESAR_L->CAESAR_TRANSITION_NUMBER]);");
|
|
| 1113 |
m_output.AppendLine("#endif");
|
|
| 1114 |
|
|
| 1115 |
m_output.AppendLine(" switch (CAESAR_L->CAESAR_TRANSITION_NUMBER)");
|
|
| 1116 |
m_output.AppendLine(" {");
|
|
| 1117 |
|
|
| 1118 |
gatenum = 0; |
|
| 1119 |
for (final NamedActionIdentifier action : actions) |
|
| 1120 |
{
|
|
| 1121 |
if (((FunctionType)action.type()).parameter().size() > 0) |
|
| 1122 |
{
|
|
| 1123 |
m_output.AppendLine(String.format(" case %1$s:", gatenum));
|
|
| 1124 |
m_output.AppendLine("#ifndef ALL_ACTIONS_VISIBLE");
|
|
| 1125 |
m_output.AppendLine("if (CAESAR_GATEKIND[CAESAR_L->CAESAR_TRANSITION_NUMBER] != INTERNAL_ACTION)");
|
|
| 1126 |
m_output.AppendLine("#endif");
|
|
| 1127 |
m_output.AppendLine("{");
|
|
| 1128 |
m_output.AppendLine(" fprintf(CAESAR_FILE,\" (\");");
|
|
| 1129 |
int paramnum = 0; |
|
| 1130 |
for (final ParameterIdentifier paramname : action.parameter()) |
|
| 1131 |
{
|
|
| 1132 |
final UlyssesType param = paramname.type(); |
|
| 1133 |
CadpType.EmitType(param); |
|
| 1134 |
m_output.AppendLine(String.format(" fprintf(CAESAR_FILE,\"%1$s: \");", paramname.tokenText()));
|
|
| 1135 |
m_output.AppendLine(String.format(" %1$s%4$s(CAESAR_FILE, CAESAR_L->CAESAR_UNION.CAESAR_PROFILE_%2$s.PARAM_%3$s);",
|
|
| 1136 |
CadpType.printString, gatenum, paramnum, CadpIdentifier.GetIdentifierString(param.identifier()))); |
|
| 1137 |
m_output.AppendLine(" fprintf(CAESAR_FILE,\" \");");
|
|
| 1138 |
paramnum++; |
|
| 1139 |
} |
|
| 1140 |
m_output.AppendLine(" fprintf(CAESAR_FILE,\")\");");
|
|
| 1141 |
m_output.AppendLine("}");
|
|
| 1142 |
m_output.AppendLine(" break;");
|
|
| 1143 |
} |
|
| 1144 |
gatenum++; |
|
| 1145 |
} |
|
| 1146 |
m_output.AppendLine(" }");
|
|
| 1147 |
rp(); |
|
| 1148 |
} |
|
| 1149 |
|
|
| 1150 |
/// <summary> |
|
| 1151 |
/// Method that exports the CAESAR_START_STATE function |
|
| 1152 |
/// </summary> |
|
| 1153 |
private void DefineCadpStartState() |
|
| 1154 |
{
|
|
| 1155 |
m_output.AppendLine("void CAESAR_START_STATE (CAESAR_TYPE_STATE CAESAR_S)");
|
|
| 1156 |
lp(); |
|
| 1157 |
m_output.AppendLine(" memset ((char *) CAESAR_S, 0, CAESAR_SIZE_STATE());");
|
|
| 1158 |
m_output.AppendLine(" Model_Reset();");
|
|
| 1159 |
for (final AttributeIdentifier x: m_statevector) |
|
| 1160 |
{
|
|
| 1161 |
m_output.Append(" CAESAR_S->");
|
|
| 1162 |
m_output.Append(x.tokenText()); |
|
| 1163 |
m_output.Append("=");
|
|
| 1164 |
final CadpType targettype = new CadpType(); |
|
| 1165 |
x.type().Accept(targettype); |
|
| 1166 |
//m_output.Append(String.format("(%1$s) ",targettype.ToString()));
|
|
| 1167 |
final CadpExpression myvis = new CadpExpression(new CadpActionInfo(null, -1, 0, "", "", "CAESAR_S")); |
|
| 1168 |
x.initializer().Accept(myvis); |
|
| 1169 |
m_output.Append(myvis.toString()); |
|
| 1170 |
m_output.AppendLine(";");
|
|
| 1171 |
} |
|
| 1172 |
rp(); |
|
| 1173 |
} |
|
| 1174 |
|
|
| 1175 |
|
|
| 1176 |
public static String FunctionHeader(FunctionIdentifier fun) |
|
| 1177 |
{
|
|
| 1178 |
return FunctionHeader(fun, fun.tokenText()); |
|
| 1179 |
} |
|
| 1180 |
|
|
| 1181 |
|
|
| 1182 |
public static String FunctionHeader(FunctionIdentifier fun, String functionName) |
|
| 1183 |
{
|
|
| 1184 |
final StringBuilder paramStr = new StringBuilder("CAESAR_TYPE_STATE CAESAR_S1");
|
|
| 1185 |
for (final ParameterIdentifier param : fun.parameter()) |
|
| 1186 |
{
|
|
| 1187 |
//CadpType.EmitType(param.type); |
|
| 1188 |
paramStr.append(", ");
|
|
| 1189 |
paramStr.append(String.format("%1$s %2$s", DumpType(param.type()), CadpIdentifier.GetIdentifierString(param)));
|
|
| 1190 |
} |
|
| 1191 |
if (((FunctionType)fun.type()).returnType() != null) |
|
| 1192 |
{
|
|
| 1193 |
//CadpType.EmitType(((FunctionType)fun.type).returnType); |
|
| 1194 |
paramStr.append(", ");
|
|
| 1195 |
paramStr.append(String.format("%1$s *param_result", DumpType(((FunctionType)fun.type()).returnType())));
|
|
| 1196 |
} |
|
| 1197 |
return String.format("struct STATE_LIST* %1$s (%2$s)", functionName, paramStr.toString());
|
|
| 1198 |
} |
|
| 1199 |
|
|
| 1200 |
public static String FunctionHeader(FunctionType fun, String functionName) |
|
| 1201 |
{
|
|
| 1202 |
final StringBuilder paramStr = new StringBuilder("CAESAR_TYPE_STATE CAESAR_S1");
|
|
| 1203 |
int i = 0; |
|
| 1204 |
for (final UlyssesType param : fun.parameter()) |
|
| 1205 |
{
|
|
| 1206 |
//CadpType.EmitType(param); |
|
| 1207 |
paramStr.append(", ");
|
|
| 1208 |
paramStr.append(String.format("%1$s param_%2$s", DumpType(param), i));
|
|
| 1209 |
i++; |
|
| 1210 |
} |
|
| 1211 |
if (fun.returnType() != null) |
|
| 1212 |
{
|
|
| 1213 |
//CadpType.EmitType(((FunctionType)fun).returnType); |
|
| 1214 |
paramStr.append(", ");
|
|
| 1215 |
paramStr.append(String.format("%1$s *param_result", DumpType(fun.returnType())));
|
|
| 1216 |
} |
|
| 1217 |
return String.format("struct STATE_LIST* %1$s (%2$s)", functionName, paramStr.toString());
|
|
| 1218 |
} |
|
| 1219 |
|
|
| 1220 |
public static final String StateVariablePrefix = "((CAESAR_TYPE_STATE)elem->aState)"; |
|
| 1221 |
|
|
| 1222 |
|
|
| 1223 |
/// <summary> |
|
| 1224 |
/// Exports a named action. |
|
| 1225 |
/// </summary> |
|
| 1226 |
private void DefineCadpAction(FunctionIdentifier action, int actionnumber) |
|
| 1227 |
{
|
|
| 1228 |
// we only want to have about 100 statements in one function so that we do not overload the |
|
| 1229 |
// stack frame with local variables. Hence we need to come up with a splitting of the |
|
| 1230 |
// statement list... We do some easy thing here and only split on the top-level sequential block. |
|
| 1231 |
final CadpActionInfo info = new CadpActionInfo(action, 10, actionnumber, "worklist", "newstatelist", "((CAESAR_TYPE_STATE)elem->aState)"); |
|
| 1232 |
final CadpStatement visitor = new CadpStatement(info); |
|
| 1233 |
action.body().Accept(visitor); |
|
| 1234 |
|
|
| 1235 |
// print out any helper code |
|
| 1236 |
final String helperMethods = info.m_helperMethods.toString(); |
|
| 1237 |
m_output.AppendLine(helperMethods); |
|
| 1238 |
m_output.AppendLine(); |
|
| 1239 |
|
|
| 1240 |
// print header of procedure |
|
| 1241 |
m_output.AppendLine(FunctionHeader(action)); |
|
| 1242 |
|
|
| 1243 |
lp(); |
|
| 1244 |
|
|
| 1245 |
for (final Identifier sym: action.symbolTable().symbolList()) |
|
| 1246 |
{
|
|
| 1247 |
if (sym.kind() == IdentifierKind.LocalVariableIdentifier) |
|
| 1248 |
{
|
|
| 1249 |
// FIXME: We need another structure for the state vars defined here, analogue to |
|
| 1250 |
// the main system state thing. Just emitting a local variable here won't cut it. |
|
| 1251 |
//throw new NotImplementedException("Local variables not supported by the CADP backend.");
|
|
| 1252 |
final CadpIdentifier ident = new CadpIdentifier(OoaCADPVisitor.StateVariablePrefix); |
|
| 1253 |
sym.Accept(ident); |
|
| 1254 |
m_output.AppendLine(String.format(" %1$s %2$s; /*local variable*/", DumpType(sym.type()), ident.toString()));
|
|
| 1255 |
} |
|
| 1256 |
} |
|
| 1257 |
|
|
| 1258 |
m_output.AppendLine(" struct STATE_LIST *worklist = NULL;");
|
|
| 1259 |
m_output.AppendLine(" struct STATE_LIST *newstatelist = NULL;");
|
|
| 1260 |
m_output.AppendLine(" LIST_INSERT_STATE(worklist,CAESAR_S1);");
|
|
| 1261 |
m_output.AppendLine(" struct STATE_LIST *_initial_worklist = worklist;");
|
|
| 1262 |
|
|
| 1263 |
m_output.AppendLine(visitor.toString()); |
|
| 1264 |
|
|
| 1265 |
|
|
| 1266 |
m_output.AppendLine(" /* delete all intermediate states. */");
|
|
| 1267 |
m_output.AppendLine(" ITERATE_STATES(newstatelist, ((CAESAR_TYPE_STATE)elem->aState)->_predecessor = CAESAR_S1;);");
|
|
| 1268 |
|
|
| 1269 |
if (actionnumber >= 0) |
|
| 1270 |
{
|
|
| 1271 |
m_output.AppendLine(String.format(" if ( newstatelist != NULL) {"));
|
|
| 1272 |
m_output.AppendLine(" CAESAR_TYPE_LABEL label;");
|
|
| 1273 |
m_output.AppendLine(" CAESAR_CREATE (label, CAESAR_SIZE_LABEL(), CAESAR_TYPE_LABEL);");
|
|
| 1274 |
m_output.AppendLine(String.format(" label->CAESAR_TRANSITION_NUMBER = %1$s;", actionnumber));
|
|
| 1275 |
int paramnumber = 0; |
|
| 1276 |
for (final ParameterIdentifier param : action.parameter()) |
|
| 1277 |
{
|
|
| 1278 |
m_output.AppendLine(String.format("label->CAESAR_UNION.CAESAR_PROFILE_%1$s.PARAM_%2$s = %3$s;", actionnumber, paramnumber, CadpIdentifier.GetIdentifierString(param)));
|
|
| 1279 |
paramnumber++; |
|
| 1280 |
} |
|
| 1281 |
m_output.AppendLine(" ITERATE_STATES(newstatelist,elem->aLabel = label;);");
|
|
| 1282 |
|
|
| 1283 |
m_output.AppendLine(" } /* newstatelist != NULL */");
|
|
| 1284 |
} |
|
| 1285 |
|
|
| 1286 |
m_output.AppendLine(" free(_initial_worklist);");
|
|
| 1287 |
|
|
| 1288 |
m_output.AppendLine(" return newstatelist;");
|
|
| 1289 |
rp(); |
|
| 1290 |
} |
|
| 1291 |
|
|
| 1292 |
/// <summary> |
|
| 1293 |
/// Exports method that calculates all reachable states from an initial state by |
|
| 1294 |
/// evaluating the do-od block once. |
|
| 1295 |
/// </summary> |
|
| 1296 |
private void DefineCadpCalculateOneIteration(Block doOdBlock) |
|
| 1297 |
{
|
|
| 1298 |
m_output.AppendLine("void OneIteration(struct STATE_LIST *worklist, struct STATE_LIST *newstatelist)");
|
|
| 1299 |
m_output.AppendLine("{");
|
|
| 1300 |
final CadpStatement visitor = new CadpStatement(new CadpActionInfo(null, -1, 0, "worklist", "newstatelist", "((CAESAR_TYPE_STATE)elem->aState)"), true); |
|
| 1301 |
doOdBlock.Accept(visitor); |
|
| 1302 |
m_output.AppendLine(visitor.toString()); |
|
| 1303 |
m_output.AppendLine("");
|
|
| 1304 |
m_output.AppendLine(" worklist = newstatelist;");
|
|
| 1305 |
m_output.AppendLine(" newstatelist = NULL;");
|
|
| 1306 |
m_output.AppendLine(" /* end states are not hidden */ ");
|
|
| 1307 |
m_output.AppendLine(" ITERATE_STATES(worklist, ((CAESAR_TYPE_STATE)elem->aState)->_hidden = 0;);");
|
|
| 1308 |
m_output.AppendLine(" /* setup tree and remove dead-ends */ ");
|
|
| 1309 |
m_output.AppendLine(" mark_tree(worklist); /*mark&sweep dead ends*/");
|
|
| 1310 |
m_output.AppendLine(" sweep_states(ARGOS_ALL_STATES);");
|
|
| 1311 |
m_output.AppendLine(" unmark_tree(worklist);");
|
|
| 1312 |
m_output.AppendLine(" connect_tree(ARGOS_ALL_STATES); /*setup successor relation*/");
|
|
| 1313 |
m_output.AppendLine(" free_allStateList(&ARGOS_ALL_STATES); /*free allstatelist and worklist*/");
|
|
| 1314 |
m_output.AppendLine("}");
|
|
| 1315 |
} |
|
| 1316 |
|
|
| 1317 |
/// <summary> |
|
| 1318 |
/// Method that exports the CAESAR_ITERATE_STATE function |
|
| 1319 |
/// </summary> |
|
| 1320 |
private void DefineCadpIterateState(OoActionSystemType system) |
|
| 1321 |
{
|
|
| 1322 |
if (system.doOdBlock() != null) |
|
| 1323 |
DefineCadpCalculateOneIteration(system.doOdBlock()); |
|
| 1324 |
|
|
| 1325 |
line(); |
|
| 1326 |
|
|
| 1327 |
m_output.AppendLine("void CAESAR_ITERATE_STATE (CAESAR_TYPE_STATE CAESAR_S1, CAESAR_TYPE_LABEL CAESAR_L, CAESAR_TYPE_STATE CAESAR_S2, void (*CAESAR_LOOP) (CAESAR_TYPE_STATE, CAESAR_TYPE_LABEL, CAESAR_TYPE_STATE))");
|
|
| 1328 |
lp(); |
|
| 1329 |
|
|
| 1330 |
m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
|
|
| 1331 |
m_output.AppendLine(" if (CAESAR_S1->_successors == NULL && CAESAR_S1->_hidden == 1)");
|
|
| 1332 |
m_output.AppendLine(" {");
|
|
| 1333 |
m_output.AppendLine(" printf(\"Re-evaluation of internal state not possible: Re-compile with UNLIMITED_REEVAL defined.\\n\");");
|
|
| 1334 |
m_output.AppendLine(" /*if you want to have this feature, you must not free the successors below. leak!*/");
|
|
| 1335 |
m_output.AppendLine(" abort();");
|
|
| 1336 |
m_output.AppendLine(" }");
|
|
| 1337 |
m_output.AppendLine("#endif");
|
|
| 1338 |
|
|
| 1339 |
m_output.AppendLine(" if (CAESAR_S1->_successors == NULL && CAESAR_S1->_hidden == 0)");
|
|
| 1340 |
m_output.AppendLine(" {");
|
|
| 1341 |
if (system.doOdBlock() != null) |
|
| 1342 |
{
|
|
| 1343 |
m_output.AppendLine(" struct STATE_LIST *worklist = NULL;");
|
|
| 1344 |
m_output.AppendLine(" struct STATE_LIST *newstatelist = NULL;");
|
|
| 1345 |
m_output.AppendLine(" LIST_INSERT_STATE(worklist,CAESAR_S1);");
|
|
| 1346 |
m_output.AppendLine(" struct STATE_LIST *initial_worklist = worklist;");
|
|
| 1347 |
m_output.AppendLine(" OneIteration(worklist, newstatelist);");
|
|
| 1348 |
m_output.AppendLine(" free(initial_worklist);");
|
|
| 1349 |
} |
|
| 1350 |
m_output.AppendLine(" } /* done calculating successors.. */");
|
|
| 1351 |
|
|
| 1352 |
m_output.AppendLine(" if (CAESAR_S1->_successors != NULL)");
|
|
| 1353 |
m_output.AppendLine(" {");
|
|
| 1354 |
m_output.AppendLine(" struct STATE_LIST *elem = CAESAR_S1->_successors;");
|
|
| 1355 |
m_output.AppendLine(" struct STATE_LIST *nelem = NULL;");
|
|
| 1356 |
m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
|
|
| 1357 |
m_output.AppendLine(" CAESAR_S1->_successors = NULL;");
|
|
| 1358 |
m_output.AppendLine("#endif");
|
|
| 1359 |
m_output.AppendLine(" while (elem != NULL)");
|
|
| 1360 |
m_output.AppendLine(" {");
|
|
| 1361 |
m_output.AppendLine(" if (elem->aLabel == NULL) {");
|
|
| 1362 |
//INTERNAL_ACTION_NUMBER |
|
| 1363 |
m_output.AppendLine(" CAESAR_TYPE_LABEL label;");
|
|
| 1364 |
m_output.AppendLine(" CAESAR_CREATE (label, CAESAR_SIZE_LABEL(), CAESAR_TYPE_LABEL);");
|
|
| 1365 |
m_output.AppendLine(" label->CAESAR_TRANSITION_NUMBER = INTERNAL_ACTION_NUMBER;");
|
|
| 1366 |
m_output.AppendLine(" elem->aLabel = label;");
|
|
| 1367 |
m_output.AppendLine(" }");
|
|
| 1368 |
m_output.AppendLine(" memcpy(CAESAR_S2,elem->aState,CAESAR_SIZE_STATE());");
|
|
| 1369 |
/* |
|
| 1370 |
m_output.AppendLine(" if (CAESAR_S2->_hidden == 1 && (int)CAESAR_S2->_statenum < 0)");
|
|
| 1371 |
m_output.AppendLine(" {");
|
|
| 1372 |
m_output.AppendLine(" printf(\"statenum not initialized: %d\\n\", (int)CAESAR_S2->_statenum);");
|
|
| 1373 |
m_output.AppendLine(" abort();");
|
|
| 1374 |
m_output.AppendLine(" }");
|
|
| 1375 |
*/ |
|
| 1376 |
m_output.AppendLine(" CAESAR_S2->_predecessor = NULL;");
|
|
| 1377 |
|
|
| 1378 |
m_output.AppendLine(" memcpy(CAESAR_L,elem->aLabel,CAESAR_SIZE_LABEL());");
|
|
| 1379 |
m_output.AppendLine(" CAESAR_LOOP(CAESAR_S1, CAESAR_L, CAESAR_S2);");
|
|
| 1380 |
m_output.AppendLine(" nelem = elem->next;");
|
|
| 1381 |
m_output.AppendLine("#ifndef UNLIMITED_REEVAL");
|
|
| 1382 |
m_output.AppendLine(" free(elem->aLabel);");
|
|
| 1383 |
m_output.AppendLine(" free(elem->aState); /*leaky: we must not free the successor list because of hidden states*/");
|
|
| 1384 |
m_output.AppendLine(" free(elem);");
|
|
| 1385 |
m_output.AppendLine("#endif");
|
|
| 1386 |
m_output.AppendLine(" elem = nelem;");
|
|
| 1387 |
m_output.AppendLine(" }");
|
|
| 1388 |
m_output.AppendLine(" }");
|
|
| 1389 |
rp(); |
|
| 1390 |
} |
|
| 1391 |
|
|
| 1392 |
} |
|
| 52 |
|
|
| 53 |
|
|
| 54 |
/* |
|
| 55 |
* OoaCADPVisitor |
|
| 56 |
* |
|
| 57 |
*/ |
|
| 58 |
|
|
| 59 |
public final class OoaCADPVisitor extends OoaCompleteAstTraversalVisitor |
|
| 60 |
{
|
|
| 61 |
final static int s_codeGenVersion = 10; |
|
| 62 |
|
|
| 63 |
private OoasCodeEmitter m_output; |
|
| 64 |
private final List<AttributeIdentifier> m_statevector; |
|
| 65 |
private final int GraphImplementationVersion = 24; |
|
| 66 |
private final List<NamedActionIdentifier> actions = new ArrayList<NamedActionIdentifier>(); |
|
| 67 |
private final List<MethodIdentifier> methods = new ArrayList<MethodIdentifier>(); |
|
| 68 |
// private final String m_AttributePre; |
|
| 69 |
public int m_internalActionNumber = 0; |
|
| 70 |
|
|
| 71 |
public static int getUIntHashCode(Object o) {
|
|
| 72 |
int hash = o.hashCode(); |
|
| 73 |
if (hash >= 0) |
|
| 74 |
return hash; |
|
| 75 |
if (hash == Integer.MIN_VALUE) |
|
| 76 |
hash +=1; |
|
| 77 |
return -hash; |
|
| 78 |
} |
|
| 79 |
|
|
| 80 |
/// <summary> |
|
| 81 |
/// Dumps a comment containing all the version information |
|
| 82 |
/// </summary> |
|
| 83 |
private void DumpHeader(OoasCodeEmitter m_output) |
|
| 84 |
{
|
|
| 85 |
m_output.AppendLine(); |
|
| 86 |
m_output.AppendLine("/* Argos Generated");
|
|
| 87 |
m_output.AppendLine(Version.asString()); |
|
| 88 |
m_output.AppendLine(String.format(" Code-Gen Version: %s", s_codeGenVersion));
|
|
| 89 |
m_output.Append(" Generated: "); m_output.AppendLine((new Date()).toString());
|
|
| 90 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 91 |
m_output.AppendLine(); |
|
| 92 |
m_output.AppendLine(" assumed data-type sizes:");
|
|
| 93 |
for( final String x : CadpType.sizeOfTypes().keySet()) |
|
| 94 |
m_output.AppendLine(String.format("%s: %s", new Object[] { x, CadpType.sizeOfTypes().get(x).toString() }));
|
|
| 95 |
m_output.AppendLine("");
|
|
| 96 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 97 |
m_output.AppendLine("------------------------------------------------------------------------");
|
|
| 98 |
m_output.AppendLine("*/");
|
|
| 99 |
} |
|
| 100 |
|
|
| 101 |
/// <summary> |
|
| 102 |
/// Prints out general definitions, includes |
|
| 103 |
/// </summary> |
|
| 104 |
private void DumpDefinitions(OoasCodeEmitter m_output) |
|
| 105 |
{
|
|
| 106 |
// write Graph version and include header |
|
| 107 |
m_output.AppendLine("/*define next symbol if you want to see named internal actions (otherwise they are mapped to 'i')*/");
|
|
| 108 |
m_output.AppendLine("#define ALL_ACTIONS_VISIBLE");
|
|
| 109 |
m_output.AppendLine("/*define next symbol if you need to re-eval internal (hidden) states - attention: memory leaks*/");
|
|
| 110 |
m_output.AppendLine("//#define UNLIMITED_REEVAL");
|
|
| 111 |
m_output.AppendLine(String.format("#define CAESAR_GRAPH_IMPLEMENTATION %s", GraphImplementationVersion));
|
|
| 112 |
m_output.AppendLine("#include \"caesar_graph.h\"");
|
|
| 113 |
m_output.AppendLine("#include \"argos_runtime.h\"");
|
|
| 114 |
m_output.AppendLine("#if defined(unix) || defined(__MACH__)");
|
|
| 115 |
m_output.AppendLine("#define UNIXPACK __attribute__((__packed__))");
|
|
| 116 |
m_output.AppendLine("#undef WINDOWSPACK");
|
|
| 117 |
m_output.AppendLine("#include <netinet/in.h>");
|
|
| 118 |
m_output.AppendLine("#else");
|
|
| 119 |
m_output.AppendLine("#include <winsock.h>");
|
|
| 120 |
m_output.AppendLine("#define WINDOWSPACK");
|
|
| 121 |
m_output.AppendLine("#define UNIXPACK");
|
|
| 122 |
m_output.AppendLine("#endif");
|
|
| 123 |
|
|
| 124 |
m_output.AppendLine(" typedef unsigned long CAESAR_TYPE_WORD;");
|
|
| 125 |
m_output.AppendLine(" #define CAESAR_WORD_SIZE (sizeof (CAESAR_TYPE_WORD))");
|
|
| 126 |
m_output.AppendLine(" #define CAESAR_FULL_MASK ((CAESAR_TYPE_WORD) ~0)");
|
|
| 127 |
|
|
| 128 |
m_output.AppendLine("");
|
|
| 129 |
m_output.AppendLine("unsigned char CALC_INVALID = 0;");
|
|
| 130 |
|
|
| 131 |
m_output.AppendLine("");
|
|
| 132 |
m_output.AppendLine("void CAESAR_TERMINATE (int CAESAR_ABORT)");
|
|
| 133 |
m_output.AppendLine("{printf(\"aborted...\"); abort();}");
|
|
| 134 |
m_output.AppendLine("");
|
|
| 135 |
} |
|
| 136 |
/// <summary> |
|
Also available in: Unified diff
changing java, cpp, hpp files to unix line endings