Method: caseASpecificationStm(ASpecificationStm, Context)

1: package org.overture.interpreter.eval;
2:
3: import java.util.List;
4: import java.util.ListIterator;
5: import java.util.Vector;
6:
7: import org.overture.ast.analysis.AnalysisException;
8: import org.overture.ast.definitions.AClassInvariantDefinition;
9: import org.overture.ast.definitions.PDefinition;
10: import org.overture.ast.expressions.PExp;
11: import org.overture.ast.intf.lex.ILexLocation;
12: import org.overture.ast.intf.lex.ILexNameToken;
13: import org.overture.ast.lex.Dialect;
14: import org.overture.ast.patterns.ASeqBind;
15: import org.overture.ast.patterns.ASetBind;
16: import org.overture.ast.patterns.ATypeBind;
17: import org.overture.ast.statements.AAlwaysStm;
18: import org.overture.ast.statements.AAnnotatedStm;
19: import org.overture.ast.statements.AApplyObjectDesignator;
20: import org.overture.ast.statements.AAssignmentStm;
21: import org.overture.ast.statements.AAtomicStm;
22: import org.overture.ast.statements.ABlockSimpleBlockStm;
23: import org.overture.ast.statements.ACallObjectStm;
24: import org.overture.ast.statements.ACallStm;
25: import org.overture.ast.statements.ACaseAlternativeStm;
26: import org.overture.ast.statements.ACasesStm;
27: import org.overture.ast.statements.AClassInvariantStm;
28: import org.overture.ast.statements.ACyclesStm;
29: import org.overture.ast.statements.ADurationStm;
30: import org.overture.ast.statements.AElseIfStm;
31: import org.overture.ast.statements.AErrorStm;
32: import org.overture.ast.statements.AExitStm;
33: import org.overture.ast.statements.AFieldObjectDesignator;
34: import org.overture.ast.statements.AFieldStateDesignator;
35: import org.overture.ast.statements.AForAllStm;
36: import org.overture.ast.statements.AForIndexStm;
37: import org.overture.ast.statements.AForPatternBindStm;
38: import org.overture.ast.statements.AIdentifierObjectDesignator;
39: import org.overture.ast.statements.AIdentifierStateDesignator;
40: import org.overture.ast.statements.AIfStm;
41: import org.overture.ast.statements.ALetBeStStm;
42: import org.overture.ast.statements.ALetStm;
43: import org.overture.ast.statements.AMapSeqStateDesignator;
44: import org.overture.ast.statements.ANewObjectDesignator;
45: import org.overture.ast.statements.ANonDeterministicSimpleBlockStm;
46: import org.overture.ast.statements.ANotYetSpecifiedStm;
47: import org.overture.ast.statements.APeriodicStm;
48: import org.overture.ast.statements.AReturnStm;
49: import org.overture.ast.statements.ASelfObjectDesignator;
50: import org.overture.ast.statements.ASkipStm;
51: import org.overture.ast.statements.ASpecificationStm;
52: import org.overture.ast.statements.ASporadicStm;
53: import org.overture.ast.statements.AStartStm;
54: import org.overture.ast.statements.AStopStm;
55: import org.overture.ast.statements.ASubclassResponsibilityStm;
56: import org.overture.ast.statements.ATixeStm;
57: import org.overture.ast.statements.ATixeStmtAlternative;
58: import org.overture.ast.statements.ATrapStm;
59: import org.overture.ast.statements.AWhileStm;
60: import org.overture.ast.statements.PStm;
61: import org.overture.ast.statements.SSimpleBlockStm;
62: import org.overture.ast.types.AUnionType;
63: import org.overture.ast.types.PType;
64: import org.overture.config.Release;
65: import org.overture.config.Settings;
66: import org.overture.interpreter.annotations.INAnnotation;
67: import org.overture.interpreter.debug.BreakpointManager;
68: import org.overture.interpreter.messages.rtlog.RTExtendedTextMessage;
69: import org.overture.interpreter.messages.rtlog.RTLogger;
70: import org.overture.interpreter.runtime.Breakpoint;
71: import org.overture.interpreter.runtime.ClassInterpreter;
72: import org.overture.interpreter.runtime.Context;
73: import org.overture.interpreter.runtime.ContextException;
74: import org.overture.interpreter.runtime.ExitException;
75: import org.overture.interpreter.runtime.ObjectContext;
76: import org.overture.interpreter.runtime.PatternMatchException;
77: import org.overture.interpreter.runtime.RootContext;
78: import org.overture.interpreter.runtime.ValueException;
79: import org.overture.interpreter.runtime.VdmRuntime;
80: import org.overture.interpreter.runtime.VdmRuntimeError;
81: import org.overture.interpreter.scheduler.BasicSchedulableThread;
82: import org.overture.interpreter.scheduler.ISchedulableThread;
83: import org.overture.interpreter.scheduler.ObjectThread;
84: import org.overture.interpreter.scheduler.PeriodicThread;
85: import org.overture.interpreter.scheduler.SharedStateListner;
86: import org.overture.interpreter.values.BooleanValue;
87: import org.overture.interpreter.values.FunctionValue;
88: import org.overture.interpreter.values.IntegerValue;
89: import org.overture.interpreter.values.MapValue;
90: import org.overture.interpreter.values.ObjectValue;
91: import org.overture.interpreter.values.OperationValue;
92: import org.overture.interpreter.values.RecordValue;
93: import org.overture.interpreter.values.SeqValue;
94: import org.overture.interpreter.values.SetValue;
95: import org.overture.interpreter.values.UndefinedValue;
96: import org.overture.interpreter.values.UpdatableValue;
97: import org.overture.interpreter.values.Value;
98: import org.overture.interpreter.values.ValueList;
99: import org.overture.interpreter.values.ValueListenerList;
100: import org.overture.interpreter.values.ValueMap;
101: import org.overture.interpreter.values.ValueSet;
102: import org.overture.interpreter.values.VoidReturnValue;
103: import org.overture.interpreter.values.VoidValue;
104: import org.overture.parser.config.Properties;
105:
106: public class StatementEvaluator extends DelegateExpressionEvaluator
107: {
108:
109:         @Override
110:         public Value caseAAlwaysStm(AAlwaysStm node, Context ctxt)
111:                         throws AnalysisException
112:         {
113:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
114:
115:                 Value rv = null;
116:                 ExitException bodyRaised = null;
117:
118:                 try
119:                 {
120:                         rv = node.getBody().apply(VdmRuntime.getStatementEvaluator(), ctxt);
121:                 } catch (ExitException e)
122:                 {
123:                         // Finally clause executes the "always" statement, but we
124:                         // re-throw this exception, unless the always clause raises one.
125:
126:                         bodyRaised = e;
127:                 } finally
128:                 {
129:                         node.getAlways().apply(VdmRuntime.getStatementEvaluator(), ctxt);
130:
131:                         if (bodyRaised != null)
132:                         {
133:                                 throw bodyRaised;
134:                         }
135:                 }
136:
137:                 return rv;
138:         }
139:
140:         @Override
141:         public Value caseAAssignmentStm(AAssignmentStm node, Context ctxt)
142:                         throws AnalysisException
143:         {
144:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
145:
146:                 Value newval = node.getExp().apply(VdmRuntime.getStatementEvaluator(), ctxt);
147:                 Value oldval = node.getTarget().apply(VdmRuntime.getStatementEvaluator(), ctxt);
148:
149:                 // Experimental hood added for DESTECS
150:                 if (Settings.dialect == Dialect.VDM_RT)
151:                 {
152:                         SharedStateListner.beforeAssignmentSet(node, oldval, newval);
153:                 }
154:
155:                 try
156:                 {
157:                         oldval.set(node.getLocation(), newval.convertTo(node.getTargetType(), ctxt), ctxt);
158:                 } catch (ValueException e)
159:                 {
160:                         VdmRuntimeError.abort(node.getLocation(), e);
161:                 }
162:
163:                 if (Settings.dialect == Dialect.VDM_RT
164:                                 && Properties.rt_log_instvarchanges)
165:                 {
166:                         ObjectValue self = ctxt.getSelf(); // May be a static
167:
168:                         // The showtrace plugin does not like "quotes", nor does it
169:                         // have a \" type convention, so we substitute for apostrophes.
170:                         String noquotes = newval.toString().replaceAll("\\\"", "\'");
171:
172:                         if (self == null)
173:                         {
174:                                 RTLogger.log(new RTExtendedTextMessage("InstVarChange -> instnm: \""
175:                                                 + node.getTarget().toString()
176:                                                 + "\""
177:                                                 + " val: \""
178:                                                 + noquotes
179:                                                 + "\""
180:                                                 + " objref: nil"
181:                                                 + " id: "
182:                                                 + BasicSchedulableThread.getThread(Thread.currentThread()).getId()));
183:                         } else
184:                         {
185:                                 RTLogger.log(new RTExtendedTextMessage("InstVarChange -> instnm: \""
186:                                                 + node.getTarget().toString()
187:                                                 + "\""
188:                                                 + " val: \""
189:                                                 + noquotes
190:                                                 + "\""
191:                                                 + " objref: "
192:                                                 + self.objectReference
193:                                                 + " id: "
194:                                                 + BasicSchedulableThread.getThread(Thread.currentThread()).getId()));
195:                         }
196:                 }
197:
198:                 return new VoidValue();
199:         }
200:
201:         @Override
202:         public Value caseAAtomicStm(AAtomicStm node, Context ctxt)
203:                         throws AnalysisException
204:         {
205:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
206:
207:                 int size = node.getAssignments().size();
208:                 ValueList targets = new ValueList(size);
209:                 ValueList values = new ValueList(size);
210:
211:                 // Rather than execute the assignment statements directly, we calculate the
212:                 // Updateable values that would be affected, and the new values to put in them.
213:                 // Note that this does not provoke any invariant checks (other than those that
214:                 // may be present in the RHS expression of each assignment).
215:
216:                 for (AAssignmentStm stmt : node.getAssignments())
217:                 {
218:                         try
219:                         {
220:                                 stmt.getLocation().hit();
221:                                 targets.add(stmt.getTarget().apply(VdmRuntime.getStatementEvaluator(), ctxt));
222:                                 values.add(stmt.getExp().apply(VdmRuntime.getStatementEvaluator(), ctxt).convertTo(stmt.getTargetType(), ctxt));
223:                         } catch (ValueException e)
224:                         {
225:                                 VdmRuntimeError.abort(node.getLocation(), e);
226:                         }
227:                 }
228:
229:                 // We make the assignments atomically by turning off thread swaps and time
230:                 // then temporarily removing the listener lists from each Updateable target.
231:                 // Then, when all assignments have been made, we check the invariants by
232:                 // passing the updated values to each listener list, as the assignment would have.
233:                 // Finally, we re-enable the thread swapping and time stepping, before returning
234:                 // a void value.
235:
236:                 try
237:                 {
238:                         ctxt.threadState.setAtomic(true);
239:                         List<ValueListenerList> listenerLists = new Vector<ValueListenerList>(size);
240:
241:                         for (int i = 0; i < size; i++)
242:                         {
243:                                 UpdatableValue target = (UpdatableValue) targets.get(i);
244:                                 listenerLists.add(target.listeners);
245:                                 target.listeners = null;
246:                                 target.set(node.getLocation(), values.get(i), ctxt); // No invariant listeners
247:                                 target.listeners = listenerLists.get(i);
248:                         }
249:
250:                         for (int i = 0; i < size; i++)
251:                         {
252:                                 ValueListenerList listeners = listenerLists.get(i);
253:
254:                                 if (listeners != null)
255:                                 {
256:                                         listeners.changedValue(node.getLocation(), values.get(i), ctxt);
257:                                 }
258:                         }
259:                 } finally
260:                 {
261:                         ctxt.threadState.setAtomic(false);
262:                 }
263:
264:                 return new VoidValue();
265:         }
266:
267:         @Override
268:         public Value caseACallObjectStm(ACallObjectStm node, Context ctxt)
269:                         throws AnalysisException
270:         {
271:                 Breakpoint breakpoint = BreakpointManager.getBreakpoint(node);
272:                 breakpoint.check(node.getLocation(), ctxt);
273:                 node.getField().getLocation().hit();
274:                 boolean endstop = breakpoint.catchReturn(ctxt);
275:
276:                 // The check above increments the hit counter for the call, but so
277:                 // do the evaluations of the designator below, so we correct the
278:                 // hit count here...
279:
280:                 node.getLocation().setHits(node.getLocation().getHits() - 1);
281:                 // node.getLocation().hits--;
282:
283:                 try
284:                 {
285:                         ValueList argValues = new ValueList();
286:
287:                         for (PExp arg: node.getArgs())
288:                         {
289:                                 argValues.add(arg.apply(VdmRuntime.getStatementEvaluator(), ctxt));
290:                         }
291:                         
292:                         // Work out the actual types of the arguments, so we bind the right op/fn
293:                         List<PType> argTypes = new Vector<PType>();
294:                         int arg = 0;
295:                         
296:                         for (PType argType: node.getField().getTypeQualifier())
297:                         {
298:                                 if (argType instanceof AUnionType)
299:                                 {
300:                                         AUnionType u = (AUnionType)argType;
301:                                         
302:                                         for (PType possible: u.getTypes())
303:                                         {
304:                                                 try
305:                                                 {
306:                                                         argValues.get(arg).convertTo(possible, ctxt);
307:                                                         argTypes.add(possible);
308:                                                         break;
309:                                                 }
310:                                                 catch (ValueException e)
311:                                                 {
312:                                                         // Try again
313:                                                 }
314:                                         }
315:                                 }
316:                                 else
317:                                 {
318:                                         argTypes.add(argType);
319:                                 }
320:                                 
321:                                 arg++;
322:                         }
323:                         
324:                         if (argTypes.size() != node.getField().getTypeQualifier().size())
325:                         {
326:                                 VdmRuntimeError.abort(node.getField().getLocation(), 4168, "Arguments do not match parameters: " + node.getField(), ctxt);
327:                         }
328:
329:                         ILexNameToken adjfield = node.getField().getModifiedName(argTypes);
330:                         ObjectValue obj = node.getDesignator().apply(VdmRuntime.getStatementEvaluator(), ctxt).objectValue(ctxt);
331:                         Value v = obj.get(adjfield, node.getExplicit());
332:
333:                         if (v == null)
334:                         {
335:                                 VdmRuntimeError.abort(node.getField().getLocation(), 4035, "Object has no field: "
336:                                                 + adjfield.getName(), ctxt);
337:                         }
338:
339:                         v = v.deref();
340:
341:                         if (v instanceof OperationValue)
342:                         {
343:                                 OperationValue op = v.operationValue(ctxt);
344:                                 Value rv = op.eval(node.getLocation(), argValues, ctxt);
345:                                 
346:                                 if (endstop && !breakpoint.isContinue(ctxt))
347:                                 {
348:                                         breakpoint.enterDebugger(ctxt);
349:                                 }
350:                                 
351:                                 return rv;
352:                         }
353:                         else
354:                         {
355:                                 FunctionValue fn = v.functionValue(ctxt);
356:                                 Value rv = fn.eval(node.getLocation(), argValues, ctxt);
357:                                 
358:                                 if (endstop && !breakpoint.isContinue(ctxt))
359:                                 {
360:                                         breakpoint.enterDebugger(ctxt);
361:                                 }
362:                                 
363:                                 return rv;
364:                         }
365:                 } catch (ValueException e)
366:                 {
367:                         return VdmRuntimeError.abort(node.getLocation(), e);
368:                 }
369:         }
370:
371:         @Override
372:         public Value caseACallStm(ACallStm node, Context ctxt)
373:                         throws AnalysisException
374:         {
375:                 Breakpoint breakpoint = BreakpointManager.getBreakpoint(node);
376:                 breakpoint.check(node.getLocation(), ctxt);
377:                 boolean endstop = breakpoint.catchReturn(ctxt);
378:
379:                 try
380:                 {
381:                         Value v = ctxt.lookup(node.getName()).deref();
382:
383:                         if (v instanceof OperationValue)
384:                         {
385:                                 OperationValue op = v.operationValue(ctxt);
386:                                 ValueList argValues = new ValueList();
387:
388:                                 for (PExp arg : node.getArgs())
389:                                 {
390:                                         argValues.add(arg.apply(VdmRuntime.getStatementEvaluator(), ctxt));
391:                                 }
392:
393:                                 Value rv = op.eval(node.getLocation(), argValues, ctxt);
394:                                 
395:                                 if (endstop && !breakpoint.isContinue(ctxt))
396:                                 {
397:                                         breakpoint.enterDebugger(ctxt);
398:                                 }
399:                                 
400:                                 return rv;
401:                         }
402:                         else
403:                         {
404:                                 FunctionValue fn = v.functionValue(ctxt);
405:                                 ValueList argValues = new ValueList();
406:
407:                                 for (PExp arg : node.getArgs())
408:                                 {
409:                                         argValues.add(arg.apply(VdmRuntime.getStatementEvaluator(), ctxt));
410:                                 }
411:
412:                                 Value rv = fn.eval(node.getLocation(), argValues, ctxt);
413:                                 
414:                                 if (endstop && !breakpoint.isContinue(ctxt))
415:                                 {
416:                                         breakpoint.enterDebugger(ctxt);
417:                                 }
418:                                 
419:                                 return rv;
420:                         }
421:                 } catch (ValueException e)
422:                 {
423:                         return VdmRuntimeError.abort(node.getLocation(), e);
424:                 }
425:         }
426:
427:         @Override
428:         public Value caseACasesStm(ACasesStm node, Context ctxt)
429:                         throws AnalysisException
430:         {
431:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
432:
433:                 Value val = node.getExp().apply(VdmRuntime.getStatementEvaluator(), ctxt);
434:
435:                 for (ACaseAlternativeStm c : node.getCases())
436:                 {
437:                         Value rv = eval(c, val, ctxt);
438:                         if (rv != null)
439:                         {
440:                                 return rv;
441:                         }
442:                 }
443:
444:                 if (node.getOthers() != null)
445:                 {
446:                         return node.getOthers().apply(VdmRuntime.getStatementEvaluator(), ctxt);
447:                 }
448:
449:                 return new VoidValue();
450:         }
451:
452:         @Override
453:         public Value caseAClassInvariantStm(AClassInvariantStm node, Context ctxt)
454:                         throws AnalysisException
455:         {
456:                 for (PDefinition d : node.getInvDefs())
457:                 {
458:                         AClassInvariantDefinition invdef = (AClassInvariantDefinition) d;
459:
460:                         try
461:                         {
462:                                 if (!invdef.getExpression().apply(VdmRuntime.getStatementEvaluator(), ctxt).boolValue(ctxt))
463:                                 {
464:                                         return new BooleanValue(false);
465:                                 }
466:                         } catch (ValueException e)
467:                         {
468:                                 VdmRuntimeError.abort(node.getLocation(), e);
469:                         }
470:                 }
471:
472:                 return new BooleanValue(true);
473:         }
474:
475:         @Override
476:         public Value caseACyclesStm(ACyclesStm node, Context ctxt)
477:                         throws AnalysisException
478:         {
479:                 node.getLocation().hit();
480:                 node.getCycles().getLocation().hit();
481:
482:                 ISchedulableThread me = BasicSchedulableThread.getThread(Thread.currentThread());
483:
484:                 if (me.inOuterTimestep())
485:                 {
486:                         // Already in a timed step, so ignore nesting
487:                         return node.getStatement().apply(VdmRuntime.getStatementEvaluator(), ctxt);
488:                 } else
489:                 {
490:                         // We disable the swapping and time (RT) as cycles evaluation should be "free".
491:                         Long cycles;
492:
493:                         try
494:                         {
495:                                 ctxt.threadState.setAtomic(true);
496:                                 cycles = node.getCycles().apply(VdmRuntime.getStatementEvaluator(), ctxt).natValue(ctxt);
497:                                 
498:                         } finally
499:                         {
500:                                 ctxt.threadState.setAtomic(false);
501:                         }
502:
503:                         me.inOuterTimestep(true);
504:                         Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), ctxt);
505:                         me.inOuterTimestep(false);
506:                         me.duration(ctxt.threadState.CPU.getDuration(cycles), ctxt, node.getLocation());
507:                         return rv;
508:                 }
509:         }
510:
511:         @Override
512:         public Value caseADurationStm(ADurationStm node, Context ctxt)
513:                         throws AnalysisException
514:         {
515:                 node.getLocation().hit();
516:                 node.getDuration().getLocation().hit();
517:
518:                 ISchedulableThread me = BasicSchedulableThread.getThread(Thread.currentThread());
519:
520:                 if (me.inOuterTimestep())
521:                 {
522:                         // Already in a timed step, so ignore nesting
523:                         return node.getStatement().apply(VdmRuntime.getStatementEvaluator(), ctxt);
524:                 } else
525:                 {
526:                         // We disable the swapping and time (RT) as duration evaluation should be "free".
527:                         long step;
528:
529:                         try
530:                         {
531:                                 ctxt.threadState.setAtomic(true);
532:                                 step = node.getDuration().apply(VdmRuntime.getStatementEvaluator(), ctxt).natValue(ctxt);
533:                         } finally
534:                         {
535:                                 ctxt.threadState.setAtomic(false);
536:                         }
537:
538:                         me.inOuterTimestep(true);
539:                         Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), ctxt);
540:                         me.inOuterTimestep(false);
541:                         me.duration(step, ctxt, node.getLocation());
542:                         return rv;
543:                 }
544:         }
545:
546:         @Override
547:         public Value caseAElseIfStm(AElseIfStm node, Context ctxt)
548:                         throws AnalysisException
549:         {
550:                 return evalElseIf(node, node.getLocation(), node.getElseIf(), node.getThenStm(), ctxt);
551:         }
552:
553:         @Override
554:         public Value caseAErrorStm(AErrorStm node, Context ctxt)
555:                         throws AnalysisException
556:         {
557:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
558:                 return VdmRuntimeError.abort(node.getLocation(), 4036, "ERROR statement reached", ctxt);
559:         }
560:
561:         @Override
562:         public Value caseAExitStm(AExitStm node, Context ctxt)
563:                         throws AnalysisException
564:         {
565:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
566:                 Value v = null;
567:
568:                 if (Settings.release == Release.VDM_10 && ctxt.threadState.isPure())
569:                 {
570:                         VdmRuntimeError.abort(node.getLocation(), 4167, "Cannot call exit in a pure operation", ctxt);
571:                 }
572:
573:                 if (node.getExpression() != null)
574:                 {
575:                         v = node.getExpression().apply(VdmRuntime.getStatementEvaluator(), ctxt);
576:                 } else
577:                 {
578:                         v = new UndefinedValue();
579:                 }
580:
581:                 throw new ExitException(v, node.getLocation(), ctxt); // BANG!!
582:         }
583:
584:         @Override
585:         public Value caseAForAllStm(AForAllStm node, Context ctxt)
586:                         throws AnalysisException
587:         {
588:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
589:
590:                 try
591:                 {
592:                         ValueSet values = node.getSet().apply(VdmRuntime.getStatementEvaluator(), ctxt).setValue(ctxt);
593:
594:                         for (Value val : values)
595:                         {
596:                                 try
597:                                 {
598:                                         Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for all", ctxt);
599:                                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getPattern(), val, ctxt));
600:                                         Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
601:
602:                                         if (!rv.isVoid())
603:                                         {
604:                                                 return rv;
605:                                         }
606:                                 } catch (PatternMatchException e)
607:                                 {
608:                                         // Ignore and try others
609:                                 }
610:                         }
611:                 } catch (ValueException e)
612:                 {
613:                         VdmRuntimeError.abort(node.getLocation(), e);
614:                 }
615:
616:                 return new VoidValue();
617:         }
618:
619:         @Override
620:         public Value caseAForIndexStm(AForIndexStm node, Context ctxt)
621:                         throws AnalysisException
622:         {
623:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
624:
625:                 try
626:                 {
627:                         long fval = node.getFrom().apply(VdmRuntime.getStatementEvaluator(), ctxt).intValue(ctxt);
628:                         long tval = node.getTo().apply(VdmRuntime.getStatementEvaluator(), ctxt).intValue(ctxt);
629:                         long bval = node.getBy() == null ? 1
630:                                         : node.getBy().apply(VdmRuntime.getStatementEvaluator(), ctxt).intValue(ctxt);
631:
632:                         if (bval == 0)
633:                         {
634:                                 VdmRuntimeError.abort(node.getLocation(), 4038, "Loop, from "
635:                                                 + fval + " to " + tval + " by " + bval
636:                                                 + " will never terminate", ctxt);
637:                         }
638:
639:                         for (long value = fval; bval > 0 && value <= tval || bval < 0
640:                                         && value >= tval; value += bval)
641:                         {
642:                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for index", ctxt);
643:                                 evalContext.put(node.getVar(), new IntegerValue(value));
644:                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
645:
646:                                 if (!rv.isVoid())
647:                                 {
648:                                         return rv;
649:                                 }
650:                         }
651:                 } catch (ValueException e)
652:                 {
653:                         VdmRuntimeError.abort(node.getLocation(), e);
654:                 }
655:
656:                 return new VoidValue();
657:         }
658:
659:         @Override
660:         public Value caseAForPatternBindStm(AForPatternBindStm node, Context ctxt)
661:                         throws AnalysisException
662:         {
663:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
664:
665:                 try
666:                 {
667:                         ValueList values = node.getExp().apply(VdmRuntime.getStatementEvaluator(), ctxt).seqValue(ctxt);
668:
669:                         if (node.getReverse())
670:                         {
671:                                 ListIterator<Value> li = values.listIterator(values.size());
672:                                 ValueList backwards = new ValueList();
673:
674:                                 while (li.hasPrevious())
675:                                 {
676:                                         backwards.add(li.previous());
677:                                 }
678:
679:                                 values = backwards;
680:                         }
681:
682:                         if (node.getPatternBind().getPattern() != null)
683:                         {
684:                                 for (Value val : values)
685:                                 {
686:                                         try
687:                                         {
688:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for pattern", ctxt);
689:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getPatternBind().getPattern(), val, ctxt));
690:                                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
691:
692:                                                 if (!rv.isVoid())
693:                                                 {
694:                                                         return rv;
695:                                                 }
696:                                         } catch (PatternMatchException e)
697:                                         {
698:                                                 // Ignore mismatches
699:                                         }
700:                                 }
701:                         }
702:                         else if (node.getPatternBind().getBind() instanceof ASetBind)
703:                         {
704:                                 ASetBind setbind = (ASetBind) node.getPatternBind().getBind();
705:                                 ValueSet set = setbind.getSet().apply(VdmRuntime.getStatementEvaluator(), ctxt).setValue(ctxt);
706:
707:                                 for (Value val : values)
708:                                 {
709:                                         try
710:                                         {
711:                                                 if (!set.contains(val))
712:                                                 {
713:                                                         VdmRuntimeError.abort(node.getLocation(), 4039, "Set bind does not contain value "
714:                                                                         + val, ctxt);
715:                                                 }
716:
717:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for set bind", ctxt);
718:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(setbind.getPattern(), val, ctxt));
719:                                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
720:
721:                                                 if (!rv.isVoid())
722:                                                 {
723:                                                         return rv;
724:                                                 }
725:                                         }
726:                                         catch (PatternMatchException e)
727:                                         {
728:                                                 // Ignore mismatches
729:                                         }
730:                                 }
731:                         }
732:                         else if (node.getPatternBind().getBind() instanceof ASeqBind)
733:                         {
734:                                 ASeqBind seqbind = (ASeqBind) node.getPatternBind().getBind();
735:                                 ValueList seq = seqbind.getSeq().apply(VdmRuntime.getStatementEvaluator(), ctxt).seqValue(ctxt);
736:
737:                                 for (Value val : values)
738:                                 {
739:                                         try
740:                                         {
741:                                                 if (!seq.contains(val))
742:                                                 {
743:                                                         VdmRuntimeError.abort(node.getLocation(), 4039, "Seq bind does not contain value "
744:                                                                         + val, ctxt);
745:                                                 }
746:
747:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for seq bind", ctxt);
748:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(seqbind.getPattern(), val, ctxt));
749:                                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
750:
751:                                                 if (!rv.isVoid())
752:                                                 {
753:                                                         return rv;
754:                                                 }
755:                                         }
756:                                         catch (PatternMatchException e)
757:                                         {
758:                                                 // Ignore mismatches
759:                                         }
760:                                 }
761:                         }
762:                         else
763:                         {
764:                                 ATypeBind typebind = (ATypeBind) node.getPatternBind().getBind();
765:
766:                                 for (Value val : values)
767:                                 {
768:                                         try
769:                                         {
770:                                                 Value converted = val.convertTo(typebind.getType(), ctxt);
771:
772:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "for type bind", ctxt);
773:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(typebind.getPattern(), converted, ctxt));
774:                                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
775:
776:                                                 if (!rv.isVoid())
777:                                                 {
778:                                                         return rv;
779:                                                 }
780:                                         } catch (PatternMatchException e)
781:                                         {
782:                                                 // Ignore mismatches
783:                                         }
784:                                 }
785:                         }
786:                 } catch (ValueException e)
787:                 {
788:                         VdmRuntimeError.abort(node.getLocation(), e);
789:                 }
790:
791:                 return new VoidValue();
792:         }
793:
794:         @Override
795:         public Value caseAIfStm(AIfStm node, Context ctxt) throws AnalysisException
796:         {
797:                 return evalIf(node, node.getLocation(), node.getIfExp(), node.getThenStm(), node.getElseIf(), node.getElseStm(), ctxt);
798:         }
799:
800:         @Override
801:         public Value caseALetBeStStm(ALetBeStStm node, Context ctxt)
802:                         throws AnalysisException
803:         {
804:                 return evalLetBeSt(node, node.getLocation(), node.getDef(), node.getSuchThat(), node.getStatement(), 4040, "statement", ctxt);
805:         }
806:
807:         @Override
808:         public Value caseALetStm(ALetStm node, Context ctxt)
809:                         throws AnalysisException
810:         {
811:                 return evalLet(node, node.getLocation(), node.getLocalDefs(), node.getStatement(), "statement", ctxt);
812:         }
813:
814:         @Override
815:         public Value caseANotYetSpecifiedStm(ANotYetSpecifiedStm node, Context ctxt)
816:                         throws AnalysisException
817:         {
818:                 return evalANotYetSpecified(node,node.getLocation(),4041,"statement", ctxt);
819:         }
820:
821:         @Override
822:         public Value caseAReturnStm(AReturnStm node, Context ctxt)
823:                         throws AnalysisException
824:         {
825:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
826:
827:                 if (node.getExpression() == null)
828:                 {
829:                         return new VoidReturnValue();
830:                 } else
831:                 {
832:                         return node.getExpression().apply(VdmRuntime.getStatementEvaluator(), ctxt);
833:                 }
834:         }
835:
836:         @Override
837:         public Value caseABlockSimpleBlockStm(ABlockSimpleBlockStm node,
838:                         Context ctxt) throws AnalysisException
839:         {
840:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
841:
842:                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "block statement", ctxt);
843:
844:                 for (PDefinition d : node.getAssignmentDefs())
845:                 {
846:                         evalContext.putList(ctxt.assistantFactory.createPDefinitionAssistant().getNamedValues(d, evalContext));
847:                 }
848:
849:                 return this.evalBlock(node, evalContext);
850:         }
851:
852:         @Override
853:         public Value caseANonDeterministicSimpleBlockStm(
854:                         ANonDeterministicSimpleBlockStm node, Context ctxt)
855:                         throws AnalysisException
856:         {
857:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
858:                 return this.evalBlock(node, ctxt);
859:         }
860:
861:         @Override
862:         public Value caseASkipStm(ASkipStm node, Context ctxt)
863:                         throws AnalysisException
864:         {
865:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
866:                 return new VoidValue();
867:         }
868:
869:         @Override
870:         public Value caseASpecificationStm(ASpecificationStm node, Context ctxt)
871:                         throws AnalysisException
872:         {
873:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
874:                 return VdmRuntimeError.abort(node.getLocation(), 4047, "Cannot execute specification statement", ctxt);
875:         }
876:
877:         @Override
878:         public Value caseAStartStm(AStartStm node, Context ctxt)
879:                         throws AnalysisException
880:         {
881:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
882:
883:                 try
884:                 {
885:                         Value value = node.getObj().apply(VdmRuntime.getStatementEvaluator(), ctxt);
886:
887:                         if (value.isType(SetValue.class))
888:                         {
889:                                 ValueSet set = value.setValue(ctxt);
890:
891:                                 for (Value v : set)
892:                                 {
893:                                         ObjectValue target = v.objectValue(ctxt);
894:                                         OperationValue op = target.getThreadOperation(ctxt);
895:
896:                                         start(node, target, op, ctxt);
897:                                 }
898:                         } else
899:                         {
900:                                 ObjectValue target = value.objectValue(ctxt);
901:                                 OperationValue op = target.getThreadOperation(ctxt);
902:
903:                                 start(node, target, op, ctxt);
904:                         }
905:
906:                         return new VoidValue();
907:                 } catch (ValueException e)
908:                 {
909:                         return VdmRuntimeError.abort(node.getLocation(), e);
910:                 }
911:         }
912:
913:         @Override
914:         public Value caseAStopStm(AStopStm node, Context ctxt)
915:                         throws AnalysisException
916:         {
917:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
918:
919:                 try
920:                 {
921:                         Value value = node.getObj().apply(VdmRuntime.getStatementEvaluator(), ctxt);
922:
923:                         if (value.isType(SetValue.class))
924:                         {
925:                                 ValueSet set = value.setValue(ctxt);
926:
927:                                 for (Value v : set)
928:                                 {
929:                                         ObjectValue target = v.objectValue(ctxt);
930:                                         stop(target, node.getLocation(), ctxt);
931:                                 }
932:                         } else
933:                         {
934:                                 ObjectValue target = value.objectValue(ctxt);
935:                                 stop(target, node.getLocation(), ctxt);
936:                         }
937:
938:                         // Cause a reschedule so that this thread is stopped, if necessary
939:                         ISchedulableThread th = BasicSchedulableThread.getThread(Thread.currentThread());
940:                         th.reschedule(ctxt, node.getLocation());
941:
942:                         return new VoidValue();
943:                 } catch (ValueException e)
944:                 {
945:                         return VdmRuntimeError.abort(node.getLocation(), e);
946:                 }
947:         }
948:
949:         private void stop(ObjectValue target, ILexLocation location, Context ctxt)
950:                         throws ValueException
951:         {
952:                 List<ISchedulableThread> threads = BasicSchedulableThread.findThreads(target);
953:                 int count = 0;
954:
955:                 if (target.getCPU() != ctxt.threadState.CPU)
956:                 {
957:                         throw new ContextException(4161, "Cannot stop object "
958:                                         + target.objectReference + " on CPU "
959:                                         + target.getCPU().getName() + " from CPU "
960:                                         + ctxt.threadState.CPU, location, ctxt);
961:                 }
962:
963:                 for (ISchedulableThread th : threads)
964:                 {
965:                         if (th instanceof ObjectThread || th instanceof PeriodicThread)
966:                         {
967:                                 if (th.stopThread()) // This may stop current thread at next reschedule
968:                                 {
969:                                         count++;
970:                                 }
971:                         }
972:                 }
973:
974:                 if (count == 0)
975:                 {
976:                         throw new ContextException(4160, "Object #"
977:                                         + target.objectReference
978:                                         + " is not running a thread to stop", location, ctxt);
979:                 }
980:         }
981:
982:         @Override
983:         public Value caseASubclassResponsibilityStm(
984:                         ASubclassResponsibilityStm node, Context ctxt)
985:                         throws AnalysisException
986:         {
987:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
988:                 return VdmRuntimeError.abort(node.getLocation(), 4048, "'is subclass responsibility' statement reached", ctxt);
989:         }
990:
991:         @Override
992:         public Value caseATixeStm(ATixeStm node, Context ctxt)
993:                         throws AnalysisException
994:         {
995:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
996:                 Value rv = null;
997:
998:                 try
999:                 {
1000:                         rv = node.getBody().apply(VdmRuntime.getStatementEvaluator(), ctxt);
1001:                 } catch (ExitException original)
1002:                 {
1003:                         ExitException last = original;
1004:
1005:                         while (true)
1006:                         {
1007:                                 Value exval = last.value;
1008:
1009:                                 try
1010:                                 {
1011:                                         for (ATixeStmtAlternative tsa : node.getTraps())
1012:                                         {
1013:                                                 rv = //ctxt.assistantFactory.createATixeStmtAlternativeAssistant().
1014:                                                                 eval(tsa, node.getLocation(), exval, ctxt);
1015:
1016:                                                 if (rv != null) // Statement was executed
1017:                                                 {
1018:                                                         return rv;
1019:                                                 }
1020:                                         }
1021:                                 } catch (ExitException ex)
1022:                                 {
1023:                                         last = ex;
1024:                                         continue;
1025:                                 }
1026:
1027:                                 throw last;
1028:                         }
1029:                 }
1030:
1031:                 return rv;
1032:         }
1033:
1034:         @Override
1035:         public Value caseATrapStm(ATrapStm node, Context ctxt)
1036:                         throws AnalysisException
1037:         {
1038:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1039:                 Value rv = null;
1040:
1041:                 try
1042:                 {
1043:                         rv = node.getBody().apply(VdmRuntime.getStatementEvaluator(), ctxt);
1044:                 } catch (ExitException e)
1045:                 {
1046:                         Value exval = e.value;
1047:
1048:                         try
1049:                         {
1050:                                 if (node.getPatternBind().getPattern() != null)
1051:                                 {
1052:                                         Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "trap pattern", ctxt);
1053:                                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getPatternBind().getPattern(), exval, ctxt));
1054:                                         rv = node.getWith().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1055:                                 }
1056:                                 else if (node.getPatternBind().getBind() instanceof ASetBind)
1057:                                 {
1058:                                         ASetBind setbind = (ASetBind) node.getPatternBind().getBind();
1059:                                         ValueSet set = setbind.getSet().apply(VdmRuntime.getStatementEvaluator(), ctxt).setValue(ctxt);
1060:
1061:                                         if (set.contains(exval))
1062:                                         {
1063:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "trap set", ctxt);
1064:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(setbind.getPattern(), exval, ctxt));
1065:                                                 rv = node.getWith().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1066:                                         }
1067:                                         else
1068:                                         {
1069:                                                 throw e;        // Propagate exception
1070:                                         }
1071:                                 }
1072:                                 else if (node.getPatternBind().getBind() instanceof ASeqBind)
1073:                                 {
1074:                                         ASeqBind seqbind = (ASeqBind) node.getPatternBind().getBind();
1075:                                         ValueList seq = seqbind.getSeq().apply(VdmRuntime.getStatementEvaluator(), ctxt).seqValue(ctxt);
1076:
1077:                                         if (seq.contains(exval))
1078:                                         {
1079:                                                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "trap seq", ctxt);
1080:                                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(seqbind.getPattern(), exval, ctxt));
1081:                                                 rv = node.getWith().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1082:                                         }
1083:                                         else
1084:                                         {
1085:                                                 throw e;        // Propagate exception
1086:                                         }
1087:                                 }
1088:                                 else
1089:                                 {
1090:                                         ATypeBind typebind = (ATypeBind) node.getPatternBind().getBind();
1091:                                         Value converted = exval.convertTo(typebind.getType(), ctxt);
1092:                                         Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "trap type", ctxt);
1093:                                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(typebind.getPattern(), converted, ctxt));
1094:                                         rv = node.getWith().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1095:                                 }
1096:                         }
1097:                         catch (ValueException ve)
1098:                         {
1099:                                 throw e;
1100:                         }
1101:                         catch (PatternMatchException pe)
1102:                         {
1103:                                 throw e;
1104:                         }
1105:                 }
1106:
1107:                 return rv;
1108:         }
1109:
1110:         @Override
1111:         public Value caseAWhileStm(AWhileStm node, Context ctxt)
1112:                         throws AnalysisException
1113:         {
1114:                 BreakpointManager.getBreakpoint(node).check(node.getLocation(), ctxt);
1115:
1116:                 try
1117:                 {
1118:                         while (node.getExp().apply(VdmRuntime.getStatementEvaluator(), ctxt).boolValue(ctxt))
1119:                         {
1120:                                 Value rv = node.getStatement().apply(VdmRuntime.getStatementEvaluator(), ctxt);
1121:
1122:                                 if (!rv.isVoid())
1123:                                 {
1124:                                         return rv;
1125:                                 }
1126:                         }
1127:                 } catch (ValueException e)
1128:                 {
1129:                         VdmRuntimeError.abort(node.getLocation(), e);
1130:                 }
1131:
1132:                 return new VoidValue();
1133:         }
1134:
1135:         @Override
1136:         public Value caseAPeriodicStm(APeriodicStm node, Context ctxt)
1137:                         throws AnalysisException
1138:         {
1139:                 final int PERIODIC = 0;
1140:                 final int JITTER = 1;
1141:                 final int DELAY = 2;
1142:                 final int OFFSET = 3;
1143:
1144:                 node.setPeriod(0L);
1145:                 node.setJitter(0L);
1146:                 node.setDelay(0L);
1147:                 node.setOffset(0L);
1148:
1149:                 for (int i = 0; i < node.getArgs().size(); i++)
1150:                 {
1151:                         PExp arg = node.getArgs().get(i);
1152:                         long value = -1;
1153:                         Value argval = null;
1154:
1155:                         try
1156:                         {
1157:                                 arg.getLocation().hit();
1158:                                 
1159:                                 try
1160:                                 {
1161:                                         // We disable the swapping and time (RT) as periodic evaluation should be "free".
1162:                                         ctxt.threadState.setAtomic(true);
1163:                                         ctxt.threadState.setPure(true);
1164:                                         argval = arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1165:                                         value = argval.intValue(ctxt);
1166:                                 }
1167:                                 finally
1168:                                 {
1169:                                         ctxt.threadState.setAtomic(false);
1170:                                         ctxt.threadState.setPure(false);
1171:                                 }
1172:                                 
1173:                                 if (value < 0)
1174:                                 {
1175:                                         VdmRuntimeError.abort(node.getLocation(), 4157, "Expecting +ive integer in periodic argument "
1176:                                                         + (i + 1) + ", was " + value, ctxt);
1177:                                 }
1178:
1179:                                 if (i == PERIODIC)
1180:                                 {
1181:                                         node.setPeriod(value);
1182:                                 } else if (i == JITTER)
1183:                                 {
1184:                                         node.setJitter(value);
1185:                                 } else if (i == DELAY)
1186:                                 {
1187:                                         node.setDelay(value);
1188:                                 } else if (i == OFFSET)
1189:                                 {
1190:                                         node.setOffset(value);
1191:                                 }
1192:                         } catch (ValueException e)
1193:                         {
1194:                                 VdmRuntimeError.abort(node.getLocation(), 4157, "Expecting +ive integer in periodic argument "
1195:                                                 + (i + 1) + ", was " + argval, ctxt);
1196:                         }
1197:                 }
1198:
1199:                 if (node.getPeriod() == 0)
1200:                 {
1201:                         VdmRuntimeError.abort(node.getLocation(), 4158, "Period argument must be non-zero, was "
1202:                                         + node.getPeriod(), ctxt);
1203:                 }
1204:
1205:                 if (node.getArgs().size() == 4)
1206:                 {
1207:                         if (node.getDelay() >= node.getPeriod())
1208:                         {
1209:                                 VdmRuntimeError.abort(node.getLocation(), 4159, "Delay argument ("
1210:                                                 + node.getDelay()
1211:                                                 + ") must be less than the period ("
1212:                                                 + node.getPeriod() + ")", ctxt);
1213:                         }
1214:                 }
1215:
1216:                 return null; // Not actually used - see StartStatement
1217:         }
1218:
1219:         @Override
1220:         public Value caseASporadicStm(ASporadicStm node, Context ctxt)
1221:                         throws AnalysisException
1222:         {
1223:                 final int MINDELAY = 0;
1224:                 final int MAXDELAY = 1;
1225:                 final int OFFSET = 2;
1226:
1227:                 node.setMinDelay(0L);
1228:                 node.setMaxDelay(0L);
1229:                 node.setOffset(0L);
1230:
1231:                 int i = 0;
1232:
1233:                 for (PExp arg : node.getArgs())
1234:                 {
1235:                         Value argval = null;
1236:                         long value = 0;
1237:
1238:                         try
1239:                         {
1240:                                 arg.getLocation().hit();
1241:
1242:                                 try
1243:                                 {
1244:                                         // We disable the swapping and time (RT) as periodic evaluation should be "free".
1245:                                         ctxt.threadState.setAtomic(true);
1246:                                         ctxt.threadState.setPure(true);
1247:                                         argval = arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1248:                                         value = argval.intValue(ctxt);
1249:                                 }
1250:                                 finally
1251:                                 {
1252:                                         ctxt.threadState.setAtomic(false);
1253:                                         ctxt.threadState.setPure(false);
1254:                                 }
1255:
1256:                                 if (value < 0)
1257:                                 {
1258:                                         VdmRuntimeError.abort(node.getLocation(), 4157, "Expecting +ive integer in sporadic argument "
1259:                                                         + (i + 1) + ", was " + value, ctxt);
1260:                                 }
1261:
1262:                                 if (i == MINDELAY)
1263:                                 {
1264:                                         node.setMinDelay(value);
1265:                                 } else if (i == MAXDELAY)
1266:                                 {
1267:                                         node.setMaxDelay(value);
1268:                                 } else if (i == OFFSET)
1269:                                 {
1270:                                         node.setOffset(value);
1271:                                 }
1272:                         } catch (ValueException e)
1273:                         {
1274:                                 VdmRuntimeError.abort(node.getLocation(), 4157, "Expecting +ive integer in sporadic argument "
1275:                                                 + (i + 1) + ", was " + argval, ctxt);
1276:                         }
1277:
1278:                         i++;
1279:                 }
1280:
1281:                 return null; // Not actually used - see StartStatement
1282:         }
1283:
1284:         @Override
1285:         public Value caseAIdentifierStateDesignator(
1286:                         AIdentifierStateDesignator node, Context ctxt)
1287:                         throws AnalysisException
1288:         {
1289:                 // We lookup the name in a context comprising only state...
1290:                 // return ctxt.getUpdateable().lookup(name.getExplicit(true));
1291:                 return ctxt.lookup(node.getName().getExplicit(true));
1292:         }
1293:
1294:         @Override
1295:         public Value caseAFieldStateDesignator(AFieldStateDesignator node,
1296:                         Context ctxt) throws AnalysisException
1297:         {
1298:                 Value result = null;
1299:
1300:                 try
1301:                 {
1302:                         result = node.getObject().apply(VdmRuntime.getStatementEvaluator(), ctxt).deref();
1303:
1304:                         if (result instanceof ObjectValue && node.getObjectfield() != null)
1305:                         {
1306:                                 ObjectValue ov = result.objectValue(ctxt);
1307:                                 Value rv = ov.get(node.getObjectfield(), false);
1308:
1309:                                 if (rv == null)
1310:                                 {
1311:                                         VdmRuntimeError.abort(node.getLocation(), 4045, "Object does not contain value for field: "
1312:                                                         + node.getField(), ctxt);
1313:                                 }
1314:
1315:                                 return rv;
1316:                         } else if (result instanceof RecordValue)
1317:                         {
1318:                                 RecordValue rec = result.recordValue(ctxt);
1319:                                 result = rec.fieldmap.get(node.getField().getName());
1320:
1321:                                 if (result == null)
1322:                                 {
1323:                                         VdmRuntimeError.abort(node.getField().getLocation(), 4037, "No such field: "
1324:                                                         + node.getField(), ctxt);
1325:                                 }
1326:
1327:                                 return result;
1328:                         }
1329:                 } catch (ValueException e)
1330:                 {
1331:                         VdmRuntimeError.abort(node.getLocation(), e);
1332:                 }
1333:
1334:                 return result;
1335:         }
1336:
1337:         @Override
1338:         public Value caseAFieldObjectDesignator(AFieldObjectDesignator node,
1339:                         Context ctxt) throws AnalysisException
1340:         {
1341:                 try
1342:                 {
1343:                         Value val = node.getObject().apply(VdmRuntime.getStatementEvaluator(), ctxt).deref();
1344:
1345:                         if (val instanceof ObjectValue && node.getField() != null)
1346:                         {
1347:                                 ObjectValue ov = val.objectValue(ctxt);
1348:                                 Value rv = ov.get(node.getField(), node.getClassName() != null);
1349:
1350:                                 if (rv == null)
1351:                                 {
1352:                                         VdmRuntimeError.abort(node.getLocation(), 4045, "Object does not contain value for field: "
1353:                                                         + node.getField(), ctxt);
1354:                                 }
1355:
1356:                                 return rv;
1357:                         } else if (val instanceof RecordValue)
1358:                         {
1359:                                 RecordValue rec = val.recordValue(ctxt);
1360:                                 Value result = rec.fieldmap.get(node.getFieldName().getName());
1361:
1362:                                 if (result == null)
1363:                                 {
1364:                                         VdmRuntimeError.abort(node.getLocation(), 4046, "No such field: "
1365:                                                         + node.getFieldName(), ctxt);
1366:                                 }
1367:
1368:                                 return result;
1369:                         } else
1370:                         {
1371:                                 return VdmRuntimeError.abort(node.getLocation(), 4020, "State value is neither a record nor an object", ctxt);
1372:                         }
1373:                 } catch (ValueException e)
1374:                 {
1375:                         return VdmRuntimeError.abort(node.getLocation(), e);
1376:                 }
1377:         }
1378:
1379:         @Override
1380:         public Value caseAMapSeqStateDesignator(AMapSeqStateDesignator node,
1381:                         Context ctxt) throws AnalysisException
1382:         {
1383:                 Value result = null;
1384:
1385:                 try
1386:                 {
1387:                         Value root = node.getMapseq().apply(VdmRuntime.getStatementEvaluator(), ctxt);
1388:                         Value index = node.getExp().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1389:
1390:                         if (root.isType(MapValue.class))
1391:                         {
1392:                                 index = index.convertTo(node.getMapType().getFrom(), ctxt);
1393:                                 ValueMap map = root.mapValue(ctxt);
1394:                                 result = map.get(index);
1395:
1396:                                 if (result == null && root instanceof UpdatableValue)
1397:                                 {
1398:                                         // Assignment to a non-existent map key creates the value
1399:                                         // in order to have it updated.
1400:
1401:                                         UpdatableValue ur = (UpdatableValue) root;
1402:                                         result = UpdatableValue.factory(ur.listeners, node.getMapType().getTo());
1403:                                         map.put(index, result);
1404:                                 }
1405:                         } else if (root.isType(SeqValue.class))
1406:                         {
1407:                                 ValueList seq = root.seqValue(ctxt);
1408:                                 int i = (int) index.intValue(ctxt) - 1;
1409:
1410:                                 if (!seq.inbounds(i))
1411:                                 {
1412:                                         if (i == seq.size())
1413:                                         {
1414:                                                 // Assignment to an index one greater than the length
1415:                                                 // creates the value in order to have it updated.
1416:
1417:                                                 UpdatableValue ur = (UpdatableValue) root;
1418:                                                 seq.add(UpdatableValue.factory(ur.listeners, node.getSeqType().getSeqof()));
1419:                                         } else
1420:                                         {
1421:                                                 VdmRuntimeError.abort(node.getExp().getLocation(), 4019, "Sequence cannot extend to key: "
1422:                                                                 + index, ctxt);
1423:                                         }
1424:                                 }
1425:
1426:                                 result = seq.get(i);
1427:                         } else
1428:                         {
1429:                                 VdmRuntimeError.abort(node.getLocation(), 4020, "State value is neither a sequence nor a map", ctxt);
1430:                         }
1431:                 } catch (ValueException e)
1432:                 {
1433:                         VdmRuntimeError.abort(node.getLocation(), e);
1434:                 }
1435:
1436:                 return result;
1437:         }
1438:
1439:         @Override
1440:         public Value caseAApplyObjectDesignator(AApplyObjectDesignator node,
1441:                         Context ctxt) throws AnalysisException
1442:         {
1443:                 try
1444:                 {
1445:                         Value uv = node.getObject().apply(VdmRuntime.getStatementEvaluator(), ctxt);
1446:                         Value v = uv.deref();
1447:
1448:                         if (v instanceof MapValue)
1449:                         {
1450:                                 ValueMap mv = v.mapValue(ctxt);
1451:                                 Value a = node.getArgs().get(0).apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1452:                                 Value rv = mv.get(a);
1453:
1454:                                 if (rv == null && uv instanceof UpdatableValue)
1455:                                 {
1456:                                         // Not already in map - get listener from root object
1457:                                         UpdatableValue ur = (UpdatableValue) uv;
1458:                                         rv = UpdatableValue.factory(ur.listeners);
1459:                                         mv.put(a, rv);
1460:                                 }
1461:
1462:                                 return rv;
1463:                         } else if (v instanceof SeqValue)
1464:                         {
1465:                                 ValueList seq = v.seqValue(ctxt);
1466:                                 Value a = node.getArgs().get(0).apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1467:                                 int i = (int) a.intValue(ctxt) - 1;
1468:
1469:                                 if (!seq.inbounds(i))
1470:                                 {
1471:                                         VdmRuntimeError.abort(node.getLocation(), 4042, "Sequence does not contain key: "
1472:                                                         + a, ctxt);
1473:                                 }
1474:
1475:                                 return seq.get(i);
1476:                         } else if (v instanceof FunctionValue)
1477:                         {
1478:                                 ValueList argvals = new ValueList();
1479:
1480:                                 for (PExp arg : node.getArgs())
1481:                                 {
1482:                                         argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1483:                                 }
1484:
1485:                                 FunctionValue fv = v.functionValue(ctxt);
1486:                                 return fv.eval(node.getLocation(), argvals, ctxt);
1487:                         } else if (v instanceof OperationValue)
1488:                         {
1489:                                 ValueList argvals = new ValueList();
1490:
1491:                                 for (PExp arg : node.getArgs())
1492:                                 {
1493:                                         argvals.add(arg.apply(VdmRuntime.getExpressionEvaluator(), ctxt));
1494:                                 }
1495:
1496:                                 OperationValue ov = v.operationValue(ctxt);
1497:                                 return ov.eval(node.getLocation(), argvals, ctxt);
1498:                         } else
1499:                         {
1500:                                 return VdmRuntimeError.abort(node.getLocation(), 4043, "Object designator is not a map, sequence, operation or function", ctxt);
1501:                         }
1502:                 } catch (ValueException e)
1503:                 {
1504:                         return VdmRuntimeError.abort(node.getLocation(), e);
1505:                 }
1506:         }
1507:         
1508:         @Override
1509:         public Value caseAAnnotatedStm(AAnnotatedStm node, Context ctxt)
1510:                         throws AnalysisException
1511:         {
1512:                 if (node.getAnnotation().getImpl() instanceof INAnnotation)
1513:                 {
1514:                         INAnnotation impl = (INAnnotation)node.getAnnotation().getImpl();
1515:                         impl.inBefore(node, ctxt);
1516:                 }
1517:                 
1518:                 Value result = node.getStmt().apply(THIS, ctxt);
1519:                 
1520:                 if (node.getAnnotation().getImpl() instanceof INAnnotation)
1521:                 {
1522:                         INAnnotation impl = (INAnnotation)node.getAnnotation().getImpl();
1523:                         impl.inAfter(node, result, ctxt);
1524:                 }
1525:
1526:                 return result;
1527:         }
1528:
1529:         @Override
1530:         public Value caseAIdentifierObjectDesignator(
1531:                         AIdentifierObjectDesignator node, Context ctxt)
1532:                         throws AnalysisException
1533:         {
1534:                 return node.getExpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1535:         }
1536:
1537:         @Override
1538:         public Value caseANewObjectDesignator(ANewObjectDesignator node,
1539:                         Context ctxt) throws AnalysisException
1540:         {
1541:                 return node.getExpression().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
1542:         }
1543:
1544:         @Override
1545:         public Value caseASelfObjectDesignator(ASelfObjectDesignator node,
1546:                         Context ctxt) throws AnalysisException
1547:         {
1548:                 return ctxt.lookup(node.getSelf());
1549:         }
1550:
1551:         private Value evalBlock(SSimpleBlockStm node, Context ctxt)
1552:                         throws AnalysisException
1553:         {
1554:                 // Note, no breakpoint check - designed to be called by eval
1555:
1556:                 for (PStm s : node.getStatements())
1557:                 {
1558:                         Value rv = s.apply(VdmRuntime.getStatementEvaluator(), ctxt);
1559:
1560:                         if (!rv.isVoid())
1561:                         {
1562:                                 return rv;
1563:                         }
1564:                 }
1565:
1566:                 return new VoidValue();
1567:         }
1568:         
1569:         public Value eval(ATixeStmtAlternative node, ILexLocation location,
1570:                         Value exval, Context ctxt) throws AnalysisException
1571:         {
1572:                 Context evalContext = null;
1573:
1574:                 try
1575:                 {
1576:                         if (node.getPatternBind().getPattern() != null)
1577:                         {
1578:                                 evalContext = new Context(ctxt.assistantFactory, location, "tixe pattern", ctxt);
1579:                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(location.getModule()).getNamedValues(node.getPatternBind().getPattern(), exval, ctxt));
1580:                         }
1581:                         else if (node.getPatternBind().getBind() instanceof ASetBind)
1582:                         {
1583:                                 ASetBind setbind = (ASetBind) node.getPatternBind().getBind();
1584:                                 ValueSet set = setbind.getSet().apply(VdmRuntime.getStatementEvaluator(), ctxt).setValue(ctxt);
1585:
1586:                                 if (set.contains(exval))
1587:                                 {
1588:                                         evalContext = new Context(ctxt.assistantFactory, location, "tixe set", ctxt);
1589:                                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(location.getModule()).getNamedValues(setbind.getPattern(), exval, ctxt));
1590:                                 }
1591:                                 else
1592:                                 {
1593:                                         evalContext = null;
1594:                                 }
1595:                         }
1596:                         else if (node.getPatternBind().getBind() instanceof ASeqBind)
1597:                         {
1598:                                 ASeqBind seqbind = (ASeqBind) node.getPatternBind().getBind();
1599:                                 ValueList seq = seqbind.getSeq().apply(VdmRuntime.getStatementEvaluator(), ctxt).seqValue(ctxt);
1600:
1601:                                 if (seq.contains(exval))
1602:                                 {
1603:                                         evalContext = new Context(ctxt.assistantFactory, location, "tixe seq", ctxt);
1604:                                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(location.getModule()).getNamedValues(seqbind.getPattern(), exval, ctxt));
1605:                                 }
1606:                                 else
1607:                                 {
1608:                                         evalContext = null;
1609:                                 }
1610:                         }
1611:                         else
1612:                         {
1613:                                 ATypeBind typebind = (ATypeBind) node.getPatternBind().getBind();
1614:                                 // Note we always perform DTC checks here...
1615:                                 Value converted = exval.convertValueTo(typebind.getType(), ctxt);
1616:                                 evalContext = new Context(ctxt.assistantFactory, location, "tixe type", ctxt);
1617:                                 evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(location.getModule()).getNamedValues(typebind.getPattern(), converted, ctxt));
1618:                         }
1619:                 } catch (ValueException ve) // Type bind convert failure
1620:                 {
1621:                         evalContext = null;
1622:                 } catch (PatternMatchException e)
1623:                 {
1624:                         evalContext = null;
1625:                 }
1626:
1627:                 return evalContext == null ? null
1628:                                 : node.getStatement().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1629:         }
1630:         
1631:         private Value eval(ACaseAlternativeStm node, Value val, Context ctxt)
1632:                         throws AnalysisException
1633:         {
1634:                 Context evalContext = new Context(ctxt.assistantFactory, node.getLocation(), "case alternative", ctxt);
1635:
1636:                 node.getPattern().getLocation().hit();
1637:                 node.getLocation().hit();
1638:                 try
1639:                 {
1640:                         evalContext.putList(ctxt.assistantFactory.createPPatternAssistant(node.getLocation().getModule()).getNamedValues(node.getPattern(), val, ctxt));
1641:                         return node.getResult().apply(VdmRuntime.getStatementEvaluator(), evalContext);
1642:                 } catch (PatternMatchException e)
1643:                 {
1644:                         // CasesStatement tries the others
1645:                 }
1646:
1647:                 return null;
1648:         }
1649:         
1650:         public void start(AStartStm node, ObjectValue target, OperationValue op,
1651:                         Context ctxt) throws AnalysisException
1652:         {
1653:                 if (op.body instanceof APeriodicStm)
1654:                 {
1655:                         RootContext global = ClassInterpreter.getInstance().initialContext;
1656:                         Context pctxt = new ObjectContext(ctxt.assistantFactory, op.name.getLocation(), "async", global, target);
1657:                         APeriodicStm ps = (APeriodicStm) op.body;
1658:
1659:                         // We disable the swapping and time (RT) as periodic evaluation should be "free".
1660:                         try
1661:                         {
1662:                                 pctxt.threadState.setAtomic(true);
1663:                                 ps.apply(VdmRuntime.getStatementEvaluator(), pctxt); // Ignore return value
1664:                         } finally
1665:                         {
1666:                                 pctxt.threadState.setAtomic(false);
1667:                         }
1668:
1669:                         OperationValue pop = pctxt.lookup(ps.getOpname()).operationValue(pctxt);
1670:
1671:                         long period = ps.getPeriod();
1672:                         long jitter = ps.getJitter();
1673:                         long delay = ps.getDelay();
1674:                         long offset = ps.getOffset();
1675:
1676:                         // Note that periodic threads never set the stepping flag
1677:
1678:                         new PeriodicThread(target, pop, period, jitter, delay, offset, 0, false).start();
1679:                 } else if (op.body instanceof ASporadicStm)
1680:                 {
1681:                         RootContext global = ClassInterpreter.getInstance().initialContext;
1682:                         Context pctxt = new ObjectContext(ctxt.assistantFactory, op.name.getLocation(), "sporadic", global, target);
1683:                         ASporadicStm ss = (ASporadicStm) op.body;
1684:
1685:                         // We disable the swapping and time (RT) as sporadic evaluation should be "free".
1686:                         try
1687:                         {
1688:                                 pctxt.threadState.setAtomic(true);
1689:                                 ss.apply(VdmRuntime.getStatementEvaluator(), pctxt); // Ignore return value
1690:                         } finally
1691:                         {
1692:                                 pctxt.threadState.setAtomic(false);
1693:                         }
1694:
1695:                         OperationValue pop = pctxt.lookup(ss.getOpname()).operationValue(pctxt);
1696:
1697:                         long delay = ss.getMinDelay();
1698:                         long jitter = ss.getMaxDelay(); // Jitter used for maximum delay
1699:                         long offset = ss.getOffset();
1700:                         long period = 0;
1701:
1702:                         // Note that periodic threads never set the stepping flag
1703:                         new PeriodicThread(target, pop, period, jitter, delay, offset, 0, true).start();
1704:                 } else
1705:                 {
1706:                         new ObjectThread(node.getLocation(), target, ctxt).start();
1707:                 }
1708:         }
1709:
1710: }