Package: Interpreter

Interpreter

nameinstructionbranchcomplexitylinemethod
Interpreter(IInterpreterAssistantFactory)
M: 0 C: 26
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
clearBreakpoint(int)
M: 55 C: 0
0%
M: 8 C: 0
0%
M: 5 C: 0
0%
M: 9 C: 0
0%
M: 1 C: 0
0%
clearBreakpointHits()
M: 9 C: 9
50%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 2 C: 2
50%
M: 0 C: 1
100%
execute(File)
M: 36 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 10 C: 0
0%
M: 1 C: 0
0%
findClass(String)
M: 9 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
findGlobal(LexNameToken)
M: 5 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
findModule(String)
M: 9 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
getAssistantFactory()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getBreakpoints()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getInitialContext()
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getInstance()
M: 0 C: 2
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getSourceFile(File)
M: 21 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 5 C: 0
0%
M: 1 C: 0
0%
getSourceLine(File, int)
M: 6 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getSourceLine(File, int, String)
M: 43 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 8 C: 0
0%
M: 1 C: 0
0%
getSourceLine(ILexLocation)
M: 7 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
runtrace(String, int, boolean)
M: 10 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
runtrace(String, int, boolean, float, TraceReductionType, long)
M: 334 C: 0
0%
M: 35 C: 0
0%
M: 19 C: 0
0%
M: 72 C: 0
0%
M: 1 C: 0
0%
setBreakpoint(PExp, String)
M: 27 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
setBreakpoint(PStm, String)
M: 27 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
setTraceOutput(PrintWriter)
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
setTracepoint(PExp, String)
M: 27 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
setTracepoint(PStm, String)
M: 27 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
static {...}
M: 2 C: 10
83%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
typeCheck(INode, Interpreter, CallSequence, Environment)
M: 0 C: 76
100%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 0 C: 15
100%
M: 0 C: 1
100%
typeCheck(PExp, Environment)
M: 5 C: 27
84%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 3 C: 7
70%
M: 0 C: 1
100%
typeCheck(PStm, Environment)
M: 5 C: 27
84%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 3 C: 7
70%
M: 0 C: 1
100%
typeCheck(String)
M: 12 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.interpreter.runtime;
25:
26: import java.io.BufferedReader;
27: import java.io.File;
28: import java.io.FileReader;
29: import java.io.IOException;
30: import java.io.PrintWriter;
31: import java.util.HashMap;
32: import java.util.List;
33: import java.util.Map;
34: import java.util.Map.Entry;
35: import java.util.Set;
36: import java.util.TreeMap;
37: import java.util.Vector;
38:
39: import org.overture.ast.analysis.AnalysisException;
40: import org.overture.ast.definitions.ANamedTraceDefinition;
41: import org.overture.ast.definitions.PDefinition;
42: import org.overture.ast.definitions.SClassDefinition;
43: import org.overture.ast.expressions.PExp;
44: import org.overture.ast.intf.lex.ILexLocation;
45: import org.overture.ast.lex.Dialect;
46: import org.overture.ast.lex.LexIdentifierToken;
47: import org.overture.ast.lex.LexNameToken;
48: import org.overture.ast.lex.LexToken;
49: import org.overture.ast.modules.AModuleModules;
50: import org.overture.ast.node.INode;
51: import org.overture.ast.statements.PStm;
52: import org.overture.ast.typechecker.NameScope;
53: import org.overture.ast.types.PType;
54: import org.overture.ast.util.modules.CombinedDefaultModule;
55: import org.overture.config.Settings;
56: import org.overture.interpreter.assistant.IInterpreterAssistantFactory;
57: import org.overture.interpreter.debug.BreakpointManager;
58: import org.overture.interpreter.debug.DBGPReader;
59: import org.overture.interpreter.messages.Console;
60: import org.overture.interpreter.scheduler.BasicSchedulableThread;
61: import org.overture.interpreter.scheduler.ResourceScheduler;
62: import org.overture.interpreter.traces.CallSequence;
63: import org.overture.interpreter.traces.TestSequence;
64: import org.overture.interpreter.traces.TraceReductionType;
65: import org.overture.interpreter.traces.TraceVariableStatement;
66: import org.overture.interpreter.traces.Verdict;
67: import org.overture.interpreter.values.Value;
68: import org.overture.parser.lex.LexException;
69: import org.overture.parser.lex.LexTokenReader;
70: import org.overture.parser.messages.VDMErrorsException;
71: import org.overture.parser.syntax.ParserException;
72: import org.overture.pog.pub.IProofObligationList;
73: import org.overture.typechecker.Environment;
74: import org.overture.typechecker.FlatEnvironment;
75: import org.overture.typechecker.ModuleEnvironment;
76: import org.overture.typechecker.PrivateClassEnvironment;
77: import org.overture.typechecker.TypeCheckInfo;
78: import org.overture.typechecker.TypeChecker;
79: import org.overture.typechecker.visitor.TypeCheckVisitor;
80:
81: /**
82: * An abstract VDM interpreter.
83: */
84:
85:•abstract public class Interpreter
86: {
87:         /** the assistant factory used by this interpreter for e.g. FunctionValues */
88:         protected final IInterpreterAssistantFactory assistantFactory;
89:
90:         /** The main thread scheduler */
91:         public ResourceScheduler scheduler;
92:
93:         /** The initial execution context. */
94:         public RootContext initialContext;
95:
96:         /** A list of breakpoints created. */
97:         public Map<Integer, Breakpoint> breakpoints;
98:
99:         /** A list of source files loaded. */
100:         public Map<File, SourceFile> sourceFiles;
101:
102:         /** The number of the next breakpoint to be created. */
103:         public int nextbreakpoint = 0;
104:
105:         /** A static instance pointer to the interpreter. */
106:         protected static Interpreter instance = null;
107:
108:         /**
109:          * Create an Interpreter.
110:          *
111:          * @param assistantFactory
112:          * the assistant factory to be used by the interpreter
113:          */
114:
115:         public Interpreter(IInterpreterAssistantFactory assistantFactory)
116:         {
117:                 scheduler = new ResourceScheduler();
118:                 breakpoints = new TreeMap<Integer, Breakpoint>();
119:                 sourceFiles = new HashMap<File, SourceFile>();
120:                 this.assistantFactory = assistantFactory;
121:                 instance = this;
122:         }
123:
124:         /**
125:          * Gets the current assistant factory
126:          *
127:          * @return
128:          */
129:         public IInterpreterAssistantFactory getAssistantFactory()
130:         {
131:                 return assistantFactory;
132:         }
133:
134:         /**
135:          * Get a string version of the environment.
136:          *
137:          * @return
138:          */
139:
140:         public String getInitialContext()
141:         {
142:                 return initialContext.toString();
143:         }
144:
145:         /**
146:          * Get the global environment.
147:          *
148:          * @return
149:          */
150:
151:         abstract public Environment getGlobalEnvironment();
152:         
153:         /**
154:          * Get the global environment for some module
155:          *
156:          * @return
157:          */
158:         abstract public Environment getGlobalEnvironment(String module);
159:
160:         /**
161:          * @return The Interpreter instance.
162:          */
163:
164:         public static Interpreter getInstance()
165:         {
166:                 return instance; // NB. last one created
167:         }
168:
169:         /**
170:          * Get the name of the default module or class. Symbols in the default module or class do not have to have their
171:          * names qualified when being referred to on the command line.
172:          *
173:          * @return The default name.
174:          */
175:
176:         abstract public String getDefaultName();
177:
178:         /**
179:          * Get the filename that contains the default module or class.
180:          *
181:          * @return The default file name.
182:          */
183:
184:         abstract public File getDefaultFile();
185:
186:         /**
187:          * Set the default module or class name.
188:          *
189:          * @param name
190:          * The default name.
191:          * @throws Exception
192:          */
193:
194:         abstract public void setDefaultName(String name) throws Exception;
195:
196:         /**
197:          * Initialize the initial context. This means that all definition initializers are re-run to put the global
198:          * environment back into its original state. This is run implicitly when the interpreter starts, but it can also be
199:          * invoked explicitly via the "init" command.
200:          *
201:          * @param dbgp
202:          */
203:
204:         abstract public void init(DBGPReader dbgp);
205:
206:         /**
207:          * Initialize the context between trace sequences. This is less thorough than the full init, since it does not reset
208:          * the scheduler for example.
209:          *
210:          * @param dbgp
211:          */
212:
213:         abstract public void traceInit(DBGPReader dbgp);
214:
215:         /**
216:          * Parse the line passed, type check it and evaluate it as an expression in the initial context.
217:          *
218:          * @param line
219:          * A VDM expression.
220:          * @param dbgp
221:          * The DBGPReader, if any
222:          * @return The value of the expression.
223:          * @throws Exception
224:          * Parser, type checking or runtime errors.
225:          */
226:
227:         abstract public Value execute(String line, DBGPReader dbgp)
228:                         throws Exception;
229:
230:         /**
231:          * Parse the content of the file passed, type check it and evaluate it as an expression in the initial context.
232:          *
233:          * @param file
234:          * A file containing a VDM expression.
235:          * @return The value of the expression.
236:          * @throws Exception
237:          * Parser, type checking or runtime errors.
238:          */
239:
240:         public Value execute(File file) throws Exception
241:         {
242:                 BufferedReader br = new BufferedReader(new FileReader(file));
243:                 StringBuilder sb = new StringBuilder();
244:
245:                 String line = br.readLine();
246:
247:•                while (line != null)
248:                 {
249:                         sb.append(line);
250:                         line = br.readLine();
251:                 }
252:
253:                 br.close();
254:
255:                 Value result = execute(sb.toString(), null);
256:
257:                 BasicSchedulableThread.terminateAll(); // NB not a session (used for tests)
258:                 return result;
259:         }
260:
261:         /**
262:          * Parse the line passed, and evaluate it as an expression in the context passed. Note that this does not type check
263:          * the expression.
264:          *
265:          * @param line
266:          * A VDM expression.
267:          * @param ctxt
268:          * The context in which to evaluate the expression.
269:          * @return The value of the expression.
270:          * @throws Exception
271:          * Parser or runtime errors.
272:          */
273:
274:         abstract public Value evaluate(String line, Context ctxt) throws Exception;
275:
276:         /**
277:          * @return The list of breakpoints currently set.
278:          */
279:
280:         public Map<Integer, Breakpoint> getBreakpoints()
281:         {
282:                 return breakpoints;
283:         }
284:
285:         /**
286:          * Get a line of a source file.
287:          *
288:          * @param src
289:          * @return
290:          */
291:
292:         public String getSourceLine(ILexLocation src)
293:         {
294:                 return getSourceLine(src.getFile(), src.getStartLine());
295:         }
296:
297:         /**
298:          * Get a line of a source file by its location.
299:          *
300:          * @param file
301:          * @param line
302:          * @return
303:          */
304:
305:         public String getSourceLine(File file, int line)
306:         {
307:                 return getSourceLine(file, line, ": ");
308:         }
309:
310:         /**
311:          * Get a line of a source file by its location.
312:          *
313:          * @param file
314:          * @param line
315:          * @param sep
316:          * @return
317:          */
318:
319:         public String getSourceLine(File file, int line, String sep)
320:         {
321:                 SourceFile source = sourceFiles.get(file);
322:
323:•                if (source == null)
324:                 {
325:                         try
326:                         {
327:                                 source = new SourceFile(file);
328:                                 sourceFiles.put(file, source);
329:                         } catch (IOException e)
330:                         {
331:                                 return "Cannot open source file: " + file;
332:                         }
333:                 }
334:
335:                 return line + sep + source.getLine(line);
336:         }
337:
338:         /**
339:          * Get an entire source file object.
340:          *
341:          * @param file
342:          * @return
343:          * @throws IOException
344:          */
345:
346:         public SourceFile getSourceFile(File file) throws IOException
347:         {
348:                 SourceFile source = sourceFiles.get(file);
349:
350:•                if (source == null)
351:                 {
352:                         source = new SourceFile(file);
353:                         sourceFiles.put(file, source);
354:                 }
355:
356:                 return source;
357:         }
358:
359:         /**
360:          * Get a list of all source files.
361:          *
362:          * @return
363:          */
364:
365:         abstract public Set<File> getSourceFiles();
366:
367:         /**
368:          * Get a list of proof obligations for the loaded specification.
369:          *
370:          * @return A list of POs.
371:          * @throws AnalysisException
372:          */
373:
374:         abstract public IProofObligationList getProofObligations()
375:                         throws AnalysisException;
376:
377:         /**
378:          * Find a statement by file name and line number.
379:          *
380:          * @param file
381:          * The name of the class/module
382:          * @param lineno
383:          * The line number
384:          * @return A Statement object if found, else null.
385:          */
386:
387:         abstract public PStm findStatement(File file, int lineno);
388:
389:         /**
390:          * Find an expression by file name and line number.
391:          *
392:          * @param file
393:          * The name of the file
394:          * @param lineno
395:          * The line number
396:          * @return An Expression object if found, else null.
397:          */
398:
399:         abstract public PExp findExpression(File file, int lineno);
400:
401:         /**
402:          * Find a global environment value by name.
403:          *
404:          * @param name
405:          * The name of the variable
406:          * @return A Value object if found, else null.
407:          */
408:
409:         public Value findGlobal(LexNameToken name)
410:         {
411:                 return initialContext.check(name);
412:         }
413:
414:         /**
415:          * Set a statement tracepoint. A tracepoint does not stop execution, but evaluates and displays an expression before
416:          * continuing.
417:          *
418:          * @param stmt
419:          * The statement to trace.
420:          * @param trace
421:          * The expression to evaluate.
422:          * @return The Breakpoint object created.
423:          * @throws Exception
424:          * Expression is not valid.
425:          */
426:
427:         public Breakpoint setTracepoint(PStm stmt, String trace) throws Exception
428:         {
429:                 BreakpointManager.setBreakpoint(stmt, new Tracepoint(stmt.getLocation(), ++nextbreakpoint, trace));
430:                 breakpoints.put(nextbreakpoint, BreakpointManager.getBreakpoint(stmt));
431:                 return BreakpointManager.getBreakpoint(stmt);
432:         }
433:
434:         /**
435:          * Set an expression tracepoint. A tracepoint does not stop execution, but evaluates an expression before
436:          * continuing.
437:          *
438:          * @param exp
439:          * The expression to trace.
440:          * @param trace
441:          * The expression to evaluate.
442:          * @return The Breakpoint object created.
443:          * @throws LexException
444:          * @throws ParserException
445:          */
446:
447:         public Breakpoint setTracepoint(PExp exp, String trace)
448:                         throws ParserException, LexException
449:         {
450:                 BreakpointManager.setBreakpoint(exp, new Tracepoint(exp.getLocation(), ++nextbreakpoint, trace));
451:                 breakpoints.put(nextbreakpoint, BreakpointManager.getBreakpoint(exp));
452:                 return BreakpointManager.getBreakpoint(exp);
453:         }
454:
455:         /**
456:          * Set a statement breakpoint. A breakpoint stops execution and allows the user to query the environment.
457:          *
458:          * @param stmt
459:          * The statement at which to stop.
460:          * @param condition
461:          * The condition when to stop.
462:          * @return The Breakpoint object created.
463:          * @throws LexException
464:          * @throws ParserException
465:          */
466:
467:         public Breakpoint setBreakpoint(PStm stmt, String condition)
468:                         throws ParserException, LexException
469:         {
470:                 BreakpointManager.setBreakpoint(stmt, new Stoppoint(stmt.getLocation(), ++nextbreakpoint, condition));
471:                 breakpoints.put(nextbreakpoint, BreakpointManager.getBreakpoint(stmt));
472:                 return BreakpointManager.getBreakpoint(stmt);
473:         }
474:
475:         /**
476:          * Set an expression breakpoint. A breakpoint stops execution and allows the user to query the environment.
477:          *
478:          * @param exp
479:          * The expression at which to stop.
480:          * @param condition
481:          * The condition when to stop.
482:          * @return The Breakpoint object created.
483:          * @throws LexException
484:          * @throws ParserException
485:          */
486:
487:         public Breakpoint setBreakpoint(PExp exp, String condition)
488:                         throws ParserException, LexException
489:         {
490:                 BreakpointManager.setBreakpoint(exp, new Stoppoint(exp.getLocation(), ++nextbreakpoint, condition));
491:                 breakpoints.put(nextbreakpoint, BreakpointManager.getBreakpoint(exp));
492:                 return BreakpointManager.getBreakpoint(exp);
493:         }
494:
495:         /**
496:          * Clear the breakpoint given by the number.
497:          *
498:          * @param bpno
499:          * The breakpoint number to remove.
500:          * @return The breakpoint object removed, or null.
501:          */
502:
503:         public Breakpoint clearBreakpoint(int bpno)
504:         {
505:                 Breakpoint old = breakpoints.remove(bpno);
506:
507:•                if (old != null)
508:                 {
509:                         PStm stmt = findStatement(old.location.getFile(), old.location.getStartLine());
510:
511:•                        if (stmt != null)
512:                         {
513:                                 BreakpointManager.setBreakpoint(stmt, new Breakpoint(stmt.getLocation()));
514:                         } else
515:                         {
516:                                 PExp exp = findExpression(old.location.getFile(), old.location.getStartLine());
517:•                                assert exp != null : "Cannot locate old breakpoint?";
518:                                 BreakpointManager.setBreakpoint(exp, new Breakpoint(exp.getLocation()));
519:                         }
520:                 }
521:
522:                 return old; // null if not found
523:         }
524:
525:         public void clearBreakpointHits()
526:         {
527:•                for (Entry<Integer, Breakpoint> e : breakpoints.entrySet())
528:                 {
529:                         e.getValue().clearHits();
530:                 }
531:         }
532:
533:         abstract protected PExp parseExpression(String line, String module)
534:                         throws Exception;
535:
536:         public PType typeCheck(PExp expr, Environment env) throws Exception
537:         {
538:                 TypeChecker.clearErrors();
539:
540:                 try
541:                 {
542:                         PType type = expr.apply(new TypeCheckVisitor(), new TypeCheckInfo(assistantFactory, env, NameScope.NAMESANDSTATE));
543:
544:•                        if (TypeChecker.getErrorCount() > 0)
545:                         {
546:                                 throw new VDMErrorsException(TypeChecker.getErrors());
547:                         }
548:
549:                         return type;
550:                 } catch (Exception e)
551:                 {
552:                         throw e;
553:                 } catch (Throwable e)
554:                 {
555:                         e.printStackTrace();
556:                 }
557:
558:                 return null;
559:
560:         }
561:
562:         public PType typeCheck(PStm stmt, Environment env) throws Exception
563:         {
564:                 TypeChecker.clearErrors();
565:                 try
566:                 {
567:                         PType type = stmt.apply(new TypeCheckVisitor(), new TypeCheckInfo(assistantFactory, env, NameScope.NAMESANDSTATE));
568:
569:•                        if (TypeChecker.getErrorCount() > 0)
570:                         {
571:                                 throw new VDMErrorsException(TypeChecker.getErrors());
572:                         }
573:
574:                         return type;
575:                 } catch (Exception e)
576:                 {
577:                         throw e;
578:                 } catch (Throwable e)
579:                 {
580:                         e.printStackTrace();
581:                 }
582:
583:                 return null;
584:         }
585:
586:         public PType typeCheck(String line) throws Exception
587:         {
588:                 PExp expr = parseExpression(line, getDefaultName());
589:                 return typeCheck(expr, getGlobalEnvironment());
590:         }
591:
592:         /**
593:          * @param classname
594:          * Unused.
595:          * @return the class found or null
596:          */
597:         public SClassDefinition findClass(String classname)
598:         {
599:•                assert false : "findClass cannot be called for modules";
600:                 return null;
601:         }
602:
603:         public abstract PType findType(String typename);
604:
605:         /**
606:          * @param module
607:          * Unused.
608:          * @return the module found or null
609:          */
610:         public AModuleModules findModule(String module)
611:         {
612:•                assert false : "findModule cannot be called for classes";
613:                 return null;
614:         }
615:
616:         private static PrintWriter writer = null;
617:
618:         public static void setTraceOutput(PrintWriter pw)
619:         {
620:                 writer = pw;
621:         }
622:
623:         abstract protected ANamedTraceDefinition findTraceDefinition(
624:                         LexNameToken name);
625:
626:         public void runtrace(String name, int testNo, boolean debug)
627:                         throws Exception
628:         {
629:                 runtrace(name, testNo, debug, 1.0F, TraceReductionType.NONE, 1234);
630:         }
631:
632:         public boolean runtrace(String name, int testNo, boolean debug,
633:                         float subset, TraceReductionType type, long seed) throws Exception
634:         {
635:                 LexTokenReader ltr = new LexTokenReader(name, Dialect.VDM_SL);
636:                 LexToken token = ltr.nextToken();
637:                 ltr.close();
638:                 LexNameToken lexname = null;
639:
640:•                switch (token.type)
641:                 {
642:                         case NAME:
643:                                 lexname = (LexNameToken) token;
644:
645:•                                if (Settings.dialect == Dialect.VDM_SL
646:•                                                && !lexname.module.equals(getDefaultName()))
647:                                 {
648:                                         setDefaultName(lexname.module);
649:                                 }
650:                                 break;
651:
652:                         case IDENTIFIER:
653:                                 lexname = new LexNameToken(getDefaultName(), (LexIdentifierToken) token);
654:                                 break;
655:
656:                         default:
657:                                 throw new Exception("Expecting trace name");
658:                 }
659:
660:                 ANamedTraceDefinition tracedef = findTraceDefinition(lexname);
661:
662:•                if (tracedef == null)
663:                 {
664:                         throw new Exception("Trace " + lexname + " not found");
665:                 }
666:
667:                 TestSequence tests = null;
668:
669:                 Context ctxt = null;
670:
671:                 ctxt = getInitialTraceContext(tracedef, debug);
672:
673:                 tests = ctxt.assistantFactory.createANamedTraceDefinitionAssistant().getTests(tracedef, ctxt, subset, type, seed);
674:
675:                 boolean wasDBGP = Settings.usingDBGP;
676:                 boolean wasCMD = Settings.usingCmdLine;
677:
678:•                if (!debug)
679:                 {
680:                         Settings.usingCmdLine = false;
681:                         Settings.usingDBGP = false;
682:                 }
683:
684:•                if (writer == null)
685:                 {
686:                         writer = Console.out;
687:                 }
688:
689:•                if (testNo > tests.size())
690:                 {
691:                         throw new Exception("Trace " + lexname + " only has "
692:                                         + tests.size() + " tests");
693:                 }
694:
695:                 int n = 1;
696:                 boolean failed = false;
697:                 writer.println("Generated " + tests.size() + " tests");
698:
699:•                for (CallSequence test : tests)
700:                 {
701:•                        if (testNo > 0 && n != testNo)
702:                         {
703:                                 n++;
704:                                 continue;
705:                         }
706:                         
707:                         INode traceContainer;
708:                         Environment rootEnv;
709:•                        if (this instanceof ClassInterpreter)
710:                         {
711:                                 traceContainer = tracedef.getClassDefinition();
712:                                 rootEnv = new PrivateClassEnvironment(getAssistantFactory(), tracedef.getClassDefinition(), getGlobalEnvironment());
713:                         } else
714:                         {
715:                                 traceContainer = tracedef.parent();
716:                                 
717:•                                if(((AModuleModules)traceContainer).getIsFlat())
718:                                 {
719:                                         //search for the combined module
720:•                                        for(AModuleModules m : ((ModuleInterpreter)this).modules)
721:                                         {
722:•                                                if(m instanceof CombinedDefaultModule)
723:                                                 {
724:                                                         traceContainer = m;
725:                                                         break;
726:                                                 }
727:                                         }
728:                                 }
729:                                 rootEnv = new ModuleEnvironment(getAssistantFactory(), (AModuleModules) traceContainer);
730:                         }
731:
732:                         List<Object> result = new Vector<>();
733:                         try
734:                         {
735:                                 typeCheck(traceContainer, this, test, rootEnv);
736:                         }
737:                         catch (Exception e)
738:                         {
739:                                 result.add(e);
740:                                 result.add(Verdict.FAILED);
741:                                 failed = true;
742:                         }
743:                         
744:                         // Bodge until we figure out how to not have explicit op names.
745:                         String clean = test.toString().replaceAll("\\.\\w+`", ".");
746:
747:•                        if (test.getFilter() > 0)
748:                         {
749:                                 writer.println("Test " + n + " = " + clean);
750:                                 writer.println("Test " + n + " FILTERED by test "
751:                                                 + test.getFilter());
752:                         } else
753:                         {
754:                                 // Initialize completely between every run...
755:                                 init(ctxt.threadState.dbgp);
756:                                 result = runOneTrace(tracedef, test, debug);
757:
758:                                 tests.filter(result, test, n);
759:                                 writer.println("Test " + n + " = " + clean);
760:                                 writer.println("Result = " + result);
761:
762:•                                if (result.lastIndexOf(Verdict.PASSED) == -1)
763:                                 {
764:                                         failed = true; // Not passed => failed.
765:                                 }
766:                         }
767:
768:                         n++;
769:                 }
770:
771:                 init(null);
772:                 Settings.usingCmdLine = wasCMD;
773:                 Settings.usingDBGP = wasDBGP;
774:
775:•                return !failed;
776:         }
777:         
778:         /**
779:          * type check a test
780:          *
781:          * @param classdef
782:          * @param interpreter
783:          * @param test
784:          * @throws AnalysisException
785:          * @throws Exception
786:          */
787:         public static void typeCheck(INode classdef, Interpreter interpreter,
788:                         CallSequence test, Environment outer) throws AnalysisException,
789:                         Exception
790:         {
791:                 FlatEnvironment env = null;
792:
793:•                if (classdef instanceof SClassDefinition)
794:                 {
795:                         env = new FlatEnvironment(interpreter.getAssistantFactory(), classdef.apply(interpreter.getAssistantFactory().getSelfDefinitionFinder()), outer);
796:                 } else
797:                 {
798:                         List<PDefinition> defs = new Vector<>();
799:                         
800:•                        if(classdef instanceof AModuleModules)
801:                         {
802:                                 defs.addAll(((AModuleModules) classdef).getDefs());
803:                         }
804:                         
805:                         env = new FlatEnvironment(interpreter.getAssistantFactory(), defs, outer);
806:                 }
807:
808:•                for (int i = 0; i < test.size(); i++)
809:                 {
810:                         PStm statement = test.get(i);
811:
812:•                        if (statement instanceof TraceVariableStatement)
813:                         {
814:                                 ((TraceVariableStatement) statement).typeCheck(env, NameScope.NAMESANDSTATE);
815:                         } else
816:                         {
817:                                 statement = statement.clone();
818:                                 test.set(i, statement);
819:                                 interpreter.typeCheck(statement, env);
820:                         }
821:                 }
822:         }
823:
824:         abstract public List<Object> runOneTrace(ANamedTraceDefinition tracedef,
825:                         CallSequence test, boolean debug) throws AnalysisException;
826:
827:         abstract public Context getInitialTraceContext(
828:                         ANamedTraceDefinition tracedef, boolean debug)
829:                         throws ValueException, AnalysisException;
830: }