diff --git a/annotations/documentation/AnnotationGuide.odt b/annotations/documentation/AnnotationGuide.odt index fe46d0e3a..e9b1b6a70 100644 Binary files a/annotations/documentation/AnnotationGuide.odt and b/annotations/documentation/AnnotationGuide.odt differ diff --git a/annotations/documentation/AnnotationGuide.pdf b/annotations/documentation/AnnotationGuide.pdf index 2e0c76dc3..8766e7dbd 100644 Binary files a/annotations/documentation/AnnotationGuide.pdf and b/annotations/documentation/AnnotationGuide.pdf differ diff --git a/lsp/src/main/java/lsp/LSPServerDebug.java b/lsp/src/main/java/lsp/LSPServerDebug.java index 06dae2929..172876e7f 100644 --- a/lsp/src/main/java/lsp/LSPServerDebug.java +++ b/lsp/src/main/java/lsp/LSPServerDebug.java @@ -129,6 +129,7 @@ public void run() catch (IOException e) { Diag.severe("LSP Server stopped: %s", e.getMessage()); + Diag.error(e); } Diag.info("LSP %s Server closing port %d", dialect, socket.getLocalPort()); diff --git a/lsp/src/main/java/lsp/LSPServerStdio.java b/lsp/src/main/java/lsp/LSPServerStdio.java index e8aece87e..9095d30ca 100644 --- a/lsp/src/main/java/lsp/LSPServerStdio.java +++ b/lsp/src/main/java/lsp/LSPServerStdio.java @@ -106,6 +106,7 @@ public void run() catch (IOException e) { Diag.error("LSP Server stopped: %s", e.getMessage()); + Diag.error(e); } } } diff --git a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java index 08ba79b95..b0b4db9ce 100644 --- a/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java +++ b/lsp/src/main/java/workspace/lenses/AbstractLaunchDebugLens.java @@ -87,7 +87,13 @@ protected JSONArray launchArgs(ProofObligation po, String defaultName, boolean d if (!apply.applyTypes.isEmpty()) { - JSONArray applyTypes = new JSONArray(apply.applyTypes); + JSONArray applyTypes = new JSONArray(); + + for (String atype: apply.applyTypes) + { + applyTypes.add(atype); + } + launchArgs.put("applyTypes", applyTypes); } diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 996748104..43baa40f3 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -84,12 +84,12 @@ public class QuickCheck { - private static final long DEFAULT_TIMEOUT = 5 * 1000; // 5s timeout + public static final long DEFAULT_TIMEOUT = 5000; // 5s timeout + private int errorCount = 0; private List strategies = null; // Configured to be used private List disabled = null; // Known, but not to be used private ProofObligationList chosen = null; - private long timeout = 0; public QuickCheck() { @@ -183,9 +183,8 @@ else if ((names.isEmpty() && instance.useByDefault()) || names.contains(instance } } - public boolean initStrategies(long timeoutSecs) + public boolean initStrategies() { - this.timeout = (timeoutSecs < 0) ? DEFAULT_TIMEOUT : timeoutSecs * 1000; boolean doChecks = true; for (QCStrategy strategy: strategies) @@ -324,8 +323,6 @@ public StrategyResults getValues(ProofObligation po) IterableContext ictxt = addTypeParams(po, ctxt); boolean hasAllValues = false; long before = System.currentTimeMillis(); - INBindingGlobals globals = INBindingGlobals.getInstance(); - globals.setTimeout(timeout); // Strategies can use this while (ictxt.hasNext()) { @@ -334,7 +331,25 @@ public StrategyResults getValues(ProofObligation po) for (QCStrategy strategy: strategies) { verbose("------------------------ Invoking %s strategy on PO #%d\n", strategy.getName(), po.number); - StrategyResults sresults = strategy.getValues(po, binds, ictxt); + StrategyResults sresults = null; + + try + { + // Suspend annotation execution by the interpreter, because the + // expansion of invariant types can invoke them. + INAnnotation.suspend(true); + + sresults = strategy.getValues(po, binds, ictxt); + } + catch (Throwable t) + { + errorln("Strategy " + strategy.getName() + " failed to generate values: " + t); + continue; + } + finally + { + INAnnotation.suspend(false); + } if (sresults.provedBy != null || sresults.disprovedBy != null) // No need to go further { @@ -465,9 +480,7 @@ else if (sresults.disprovedBy != null) } } - globals.setTimeout(timeout); globals.setAllValues(sresults.hasAllValues); - Context ctxt = Interpreter.getInstance().getInitialContext(); Interpreter.getInstance().setDefaultName(po.location.module); @@ -476,6 +489,7 @@ else if (sresults.disprovedBy != null) Value execResult = new BooleanValue(false); ContextException execException = null; boolean execCompleted = false; + boolean timedOut = false; long before = System.currentTimeMillis(); try @@ -499,7 +513,8 @@ else if (sresults.disprovedBy != null) { if (e.rawMessage.equals("Execution cancelled")) { - execResult = null; + execResult = new BooleanValue(false); + timedOut = true; } else if (e.number == 4024) // 'not yet specified' expression reached { @@ -519,14 +534,7 @@ else if (e.number == 4024) // 'not yet specified' expression reached long after = System.currentTimeMillis() + sresults.duration; - if (execResult == null) // cancelled - { - infoln("----"); - printBindings(bindings); - infoln("----"); - infoln(po); - } - else if (execResult instanceof BooleanValue) + if (execResult instanceof BooleanValue) { if (execResult.boolValue(ctxt)) { @@ -534,8 +542,10 @@ else if (execResult instanceof BooleanValue) String desc = ""; po.setWitness(null); po.setProvedBy(null); + po.setCounterexample(null); + po.setMessage(null); - if (globals.didTimeout()) + if (timedOut) { outcome = POStatus.TIMEOUT; } @@ -558,8 +568,17 @@ else if (po.isExistential()) else if (sresults.hasAllValues && execCompleted) { outcome = POStatus.PROVABLE; // All values were tested and passed, so PROVABLE - desc = " by finite types"; - po.setProvedBy("finite"); + + if (bindings.isEmpty()) + { + desc = " in all cases"; + po.setProvedBy("fixed"); + } + else + { + desc = " by finite types"; + po.setProvedBy("finite"); + } } else { @@ -568,12 +587,10 @@ else if (sresults.hasAllValues && execCompleted) infof(outcome, "PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), desc, duration(before, after)); po.setStatus(outcome); - po.setCounterexample(null); - po.setMessage(null); } else { - if (globals.didTimeout()) // Result would have been true (above), but... + if (timedOut) // Result would have been true (above), but... { infof(POStatus.TIMEOUT, "PO #%d, TIMEOUT %s\n", po.number, duration(before, after)); po.setStatus(POStatus.TIMEOUT); @@ -614,7 +631,16 @@ else if (globals.hasMaybe() && execCompleted) infof(POStatus.FAILED, "PO #%d, FAILED %s: ", po.number, duration(before, after)); po.setStatus(POStatus.FAILED); printCounterexample(bindings); - po.setCounterexample(globals.getCounterexample()); + + if (bindings.isEmpty()) // Failed with no binds - eg. Test() with no params + { + po.setCounterexample(new Context(po.location, "Empty", null)); + } + else + { + po.setCounterexample(globals.getCounterexample()); + } + po.setWitness(null); if (execException != null) @@ -929,8 +955,8 @@ public void printHelp(String USAGE) println(USAGE); println(""); println(" -?|-help - show command help"); - println(" -q|-v - run with minimal or verbose output"); - println(" -t - timeout in secs"); + println(" -q|-v|-n - run with minimal, verbose, basic output"); + println(" -t - timeout in millisecs"); println(" -i - only show this result status"); println(" -s - enable this strategy (below)"); println(" - - pass option to strategy"); diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java index 68520c799..f1c8c8da3 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java @@ -59,10 +59,20 @@ public static void setIncludes(List includes) QCConsole.includes = includes; } + public static List getIncludes() + { + return includes; + } + public static void setVerbose(boolean verbose) { QCConsole.verbose = verbose; } + + public boolean getVerbose() + { + return verbose; + } public static void info(POStatus status, String m) { diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 1529af667..04a20d3a6 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -34,8 +34,9 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.debug.ConsoleDebugReader; -import com.fujitsu.vdmj.debug.ConsoleKeyWatcher; +import com.fujitsu.vdmj.debug.ConsoleExecTimer; import com.fujitsu.vdmj.lex.Dialect; +import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.plugins.AnalysisCommand; import com.fujitsu.vdmj.plugins.PluginRegistry; import com.fujitsu.vdmj.plugins.analyses.POPlugin; @@ -48,11 +49,11 @@ public class QuickCheckCommand extends AnalysisCommand { - private final static String CMD = "quickcheck [-?|-help][-q|-v][-t ][-i ]*[-s ]* [-]* []"; + private final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t ][-i ]*[-s ]* [-]* []"; private final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; public final static String HELP = SHORT + " - lightweight PO verification"; - + public QuickCheckCommand(String line) { super(line); @@ -70,6 +71,7 @@ public String run(String line) List poNames = new Vector(); List includes = new Vector(); long timeout = -1; + boolean numbersOnly = false; QuickCheck qc = new QuickCheck(); @@ -122,6 +124,11 @@ public String run(String line) return USAGE; } break; + + case "-n": + numbersOnly = true; + QCConsole.setQuiet(true); + break; case "-": i++; @@ -185,8 +192,10 @@ public String run(String line) println("No POs in current " + (Settings.dialect == Dialect.VDM_SL ? "module" : "class")); return null; } - - if (qc.initStrategies(timeout)) + + timeout = (timeout < 0) ? QuickCheck.DEFAULT_TIMEOUT : timeout; + + if (qc.initStrategies()) { for (ProofObligation po: chosen) { @@ -195,17 +204,25 @@ public String run(String line) if (!qc.hasErrors()) { - ConsoleKeyWatcher watcher = null; + ConsoleExecTimer execTimer = null; ConsoleDebugReader dbg = null; try { dbg = new ConsoleDebugReader(); dbg.start(); - watcher = new ConsoleKeyWatcher(line); - watcher.start(); + execTimer = new ConsoleExecTimer(timeout); + execTimer.start(); qc.checkObligation(po, results); + + if (numbersOnly) + { + if (includes.isEmpty() || includes.contains(po.status)) + { + Console.out.printf("PO #%d: %s\n", po.number, po.status.toString().toUpperCase()); + } + } } catch (Exception e) { @@ -213,9 +230,9 @@ public String run(String line) } finally { - if (watcher != null) + if (execTimer != null) { - watcher.interrupt(); + execTimer.interrupt(); } if (dbg != null) diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java index fed17f1ee..d0e85bfdb 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java @@ -28,7 +28,10 @@ import java.util.List; import com.fujitsu.vdmj.Settings; +import com.fujitsu.vdmj.debug.ConsoleExecTimer; import com.fujitsu.vdmj.lex.Dialect; +import com.fujitsu.vdmj.messages.Console; +import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -49,15 +52,18 @@ public class QuickCheckExecutor extends AsyncExecutor private final long timeout; private final List poList; private final List poNames; + private final boolean numbersOnly; private String answer; - public QuickCheckExecutor(DAPRequest request, QuickCheck qc, long timeout, List poList, List poNames) + public QuickCheckExecutor(DAPRequest request, QuickCheck qc, + long timeout, List poList, List poNames, boolean numbersOnly) { super("qc", request); this.qc = qc; this.timeout = timeout; this.poList = poList; this.poNames = poNames; + this.numbersOnly = numbersOnly; } @Override @@ -72,6 +78,7 @@ protected void exec() throws Exception POPlugin pog = PluginRegistry.getInstance().getPlugin("PO"); ProofObligationList all = pog.getProofObligations(); ProofObligationList chosen = qc.getPOs(all, poList, poNames); + List includes = QCConsole.getIncludes(); if (qc.hasErrors()) { @@ -85,7 +92,7 @@ protected void exec() throws Exception return; } - if (qc.initStrategies(timeout)) + if (qc.initStrategies()) { for (ProofObligation po: chosen) { @@ -93,7 +100,30 @@ protected void exec() throws Exception if (!qc.hasErrors()) { - qc.checkObligation(po, results); + ConsoleExecTimer execTimer = null; + + try + { + execTimer = new ConsoleExecTimer(timeout); + execTimer.start(); + + qc.checkObligation(po, results); + + if (numbersOnly) + { + if (includes.isEmpty() || includes.contains(po.status)) + { + Console.out.printf("PO #%d: %s\n", po.number, po.status.toString().toUpperCase()); + } + } + } + finally + { + if (execTimer != null) + { + execTimer.interrupt(); + } + } } if (cancelled) diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java index 9d870fe7e..b46a86219 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -43,7 +43,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable { - public final static String CMD = "quickcheck [-?|-help][-q|-v][-t ][-i ]*[-s ]* [-]* []"; + public final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t ][-i ]*[-s ]* [-]* []"; public final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; @@ -51,6 +51,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnabl private List poNames = new Vector(); private List includes = new Vector(); private long timeout = -1; + private boolean numbersOnly = false; private QuickCheck qc = new QuickCheck(); public QuickCheckLSPCommand(String line) @@ -125,6 +126,11 @@ private DAPMessageList setup(DAPRequest request) return result(request, USAGE); } break; + + case "-n": + QCConsole.setQuiet(true); + numbersOnly = true; + break; case "-": i++; @@ -172,6 +178,7 @@ private DAPMessageList setup(DAPRequest request) } QCConsole.setIncludes(includes); + timeout = (timeout < 0) ? QuickCheck.DEFAULT_TIMEOUT : timeout; return null; } @@ -183,7 +190,7 @@ public DAPMessageList run(DAPRequest request) if (errs == null) { - QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames); + QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames, numbersOnly); executor.start(); } @@ -199,7 +206,7 @@ public String initRun(DAPRequest request) { try { - QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames); + QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames, numbersOnly); executor.exec(); // Note, not start! executor.clean(); // Send POG updated notification return executor.getAnswer(); diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index c9e936910..573d60d60 100644 --- a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -119,7 +119,7 @@ else if (CancellableThread.currentlyRunning() != null) Vector poList = new Vector(); Vector poNames = new Vector(); - long timeout = 1L; + long timeout = 0; if (request.get("params") != null) { @@ -129,7 +129,9 @@ else if (CancellableThread.currentlyRunning() != null) { JSONObject config = params.get("config"); JSONArray obligations = config.get("obligations"); - timeout = config.get("timeout", 1L); + + timeout = config.get("timeout", 1000L); // faster for GUI? + if (timeout == 5) timeout = 5000; // HACK until GUI fixed if (obligations != null && !obligations.isEmpty()) { @@ -160,9 +162,9 @@ else if (chosen.isEmpty()) Diag.error("No POs in scope"); return new RPCMessageList(request, RPCErrors.InternalError, "No POs in scope"); } - else if (qc.initStrategies(timeout)) + else if (qc.initStrategies()) { - QuickCheckThread executor = new QuickCheckThread(request, qc, chosen); + QuickCheckThread executor = new QuickCheckThread(request, qc, chosen, timeout); executor.start(); } else diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java index a7885e2cf..3521287be 100644 --- a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckThread.java @@ -28,6 +28,7 @@ import java.util.List; import java.util.Vector; +import com.fujitsu.vdmj.debug.ConsoleExecTimer; import com.fujitsu.vdmj.messages.VDMMessage; import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.pog.POStatus; @@ -57,14 +58,16 @@ public class QuickCheckThread extends CancellableThread private final ProofObligationList chosen; private final POPlugin pog; private final Object workDoneToken; + private final long timeout; - public QuickCheckThread(RPCRequest request, QuickCheck qc, ProofObligationList chosen) + public QuickCheckThread(RPCRequest request, QuickCheck qc, ProofObligationList chosen, long timeout) { super(request.get("id")); this.request = request; this.qc = qc; this.chosen = chosen; this.pog = PluginRegistry.getInstance().getPlugin("PO"); + this.timeout = timeout; JSONObject params = request.get("params"); this.workDoneToken = params.get("workDoneToken"); @@ -93,7 +96,22 @@ protected void body() if (!qc.hasErrors()) { - qc.checkObligation(po, results); + ConsoleExecTimer execTimer = null; + + try + { + execTimer = new ConsoleExecTimer(timeout); + execTimer.start(); + + qc.checkObligation(po, results); + } + finally + { + if (execTimer != null) + { + execTimer.interrupt(); + } + } } list.add(getQCResponse(po, messages)); diff --git a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java index f4bb9592a..e96267ef8 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/DirectQCStrategy.java @@ -38,7 +38,6 @@ import com.fujitsu.vdmj.in.expressions.INCasesExpression; import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.expressions.INExpressionList; -import com.fujitsu.vdmj.in.patterns.INBindingGlobals; import com.fujitsu.vdmj.in.patterns.INBindingOverride; import com.fujitsu.vdmj.in.types.visitors.INGetAllValuesVisitor; import com.fujitsu.vdmj.in.types.visitors.INTypeSizeVisitor; @@ -161,8 +160,6 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po) if (cases != null) // Should always be found, but... { ValueList values = po.exp.expType.apply(new INGetAllValuesVisitor(), ctxt); - long timeout = INBindingGlobals.getInstance().getTimeout(); - verbose("Checking %d values of type %s\n", values.size(), po.exp.expType); for (Value value: values) @@ -192,11 +189,6 @@ private StrategyResults directCasesObligation(CasesExhaustiveObligation po) cex.put(name, value); return new StrategyResults(getName(), cex, "(case unmatched)", System.currentTimeMillis() - before); } - - if (System.currentTimeMillis() - before > timeout) - { - return new StrategyResults(); // Maybe, for very large types - } } return new StrategyResults(getName(), "(patterns match all type values)", null, System.currentTimeMillis() - before); diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index 2012f206e..6946eb68f 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -1000,3 +1000,4 @@ as the expected and actual values. 5041, "Add explicit type here"); 5042, "Missing type import for "; 5043, "Strict: Should not use 'DEFAULT' as a module name" +5044, "Annotations: " diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleExecTimer.java b/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleExecTimer.java new file mode 100644 index 000000000..18cc2e5bf --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleExecTimer.java @@ -0,0 +1,58 @@ +/******************************************************************************* + * + * Copyright (c) 202 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package com.fujitsu.vdmj.debug; + +import com.fujitsu.vdmj.runtime.Breakpoint; + +/** + * Thread to interrupt the execution of something after a certain time. + */ +public class ConsoleExecTimer extends Thread +{ + private final long timer; + + public ConsoleExecTimer(long timer) + { + this.timer = timer; + setName("ExecTimer"); + } + + @Override + public void run() + { + if (timer > 0) + { + try + { + Thread.sleep(timer); + Breakpoint.setExecInterrupt(Breakpoint.TERMINATE); + } + catch (InterruptedException e) + { + return; + } + } + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java index 7e4af2954..be81d415f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java @@ -65,8 +65,6 @@ public String toString() public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - long start = System.currentTimeMillis(); - long timeout = globals == null ? 0 : globals.getTimeout(); try { @@ -87,21 +85,6 @@ public Value eval(Context ctxt) while (quantifiers.hasNext()) { - if (timeout > 0) - { - if (System.currentTimeMillis() - start > timeout) - { - if (globals != null) - { - globals.setWitness(null); - globals.setDidTimeout(true); - globals.setMaybe(true); - } - - return new BooleanValue(true); - } - } - Context evalContext = new Context(location, "exists", ctxt); NameValuePairList nvpl = quantifiers.next(); boolean matches = true; @@ -131,7 +114,6 @@ public Value eval(Context ctxt) if (globals != null) { globals.setWitness(evalContext); - globals.setDidTimeout(false); globals.setMaybe(false); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java index 5fd89efb5..5025f6983 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java @@ -68,8 +68,6 @@ public String toString() public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - long start = System.currentTimeMillis(); - long timeout = globals == null ? 0 : globals.getTimeout(); try { @@ -90,21 +88,6 @@ public Value eval(Context ctxt) while (quantifiers.hasNext()) { - if (timeout > 0) - { - if (System.currentTimeMillis() - start > timeout) - { - if (globals != null) - { - globals.setCounterexample(null); - globals.setDidTimeout(true); - globals.setMaybe(true); - } - - return new BooleanValue(true); - } - } - Context evalContext = new Context(location, "forall", ctxt); NameValuePairList nvpl = quantifiers.next(); boolean matches = true; @@ -134,7 +117,6 @@ public Value eval(Context ctxt) if (globals != null) { globals.setCounterexample(evalContext); - globals.setDidTimeout(false); globals.setMaybe(false); } @@ -146,7 +128,6 @@ public Value eval(Context ctxt) if (globals != null) { globals.setCounterexample(evalContext); - globals.setDidTimeout(false); globals.setMaybe(false); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingGlobals.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingGlobals.java index 9218b3538..126003a3a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingGlobals.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingGlobals.java @@ -43,8 +43,6 @@ public static synchronized INBindingGlobals getInstance() private Context bindCounterexample = null; private Context bindWitness = null; private boolean bindAllValues = false; - private long bindTimeout = 0; - private boolean didTimeout = false; private boolean maybe = false; private INBindingGlobals() @@ -57,21 +55,9 @@ public void clear() bindCounterexample = null; bindWitness = null; bindAllValues = false; - bindTimeout = 0; - didTimeout = false; maybe = false; } - public void setTimeout(long timeout) - { - bindTimeout = timeout; - } - - public long getTimeout() - { - return bindTimeout; - } - public void setAllValues(boolean hasAllValues) { bindAllValues = hasAllValues; @@ -82,16 +68,6 @@ public boolean hasAllValues() return this.bindAllValues; } - public void setDidTimeout(boolean did) - { - this.didTimeout = did; - } - - public boolean didTimeout() - { - return this.didTimeout; - } - public void setCounterexample(Context ctxt) { if (ctxt == null) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/types/visitors/INInstantiateVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/types/visitors/INInstantiateVisitor.java index 96023b1bf..00da4c2d0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/types/visitors/INInstantiateVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/types/visitors/INInstantiateVisitor.java @@ -33,7 +33,9 @@ import com.fujitsu.vdmj.tc.types.TCOptionalType; import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCProductType; +import com.fujitsu.vdmj.tc.types.TCSeq1Type; import com.fujitsu.vdmj.tc.types.TCSeqType; +import com.fujitsu.vdmj.tc.types.TCSet1Type; import com.fujitsu.vdmj.tc.types.TCSetType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -55,47 +57,41 @@ public TCType caseType(TCType type, Context params) } @Override - public TCType caseBracketType(TCBracketType type, Context params) + public TCType caseBracketType(TCBracketType btype, Context params) { - TCBracketType btype = (TCBracketType) type; return new TCBracketType(btype.type.apply(this, params)); } @Override - public TCType caseInMapType(TCInMapType type, Context params) + public TCType caseInMapType(TCInMapType mtype, Context params) { - TCInMapType mtype = (TCInMapType) type; - return new TCInMapType(type.location, mtype.from.apply(this, params), mtype.to.apply(this, params)); + return new TCInMapType(mtype.location, mtype.from.apply(this, params), mtype.to.apply(this, params)); } @Override - public TCType caseMapType(TCMapType type, Context params) + public TCType caseMapType(TCMapType mtype, Context params) { - TCMapType mtype = (TCMapType) type; - return new TCMapType(type.location, mtype.from.apply(this, params), mtype.to.apply(this, params)); + return new TCMapType(mtype.location, mtype.from.apply(this, params), mtype.to.apply(this, params)); } @Override - public TCType caseOptionalType(TCOptionalType type, Context params) + public TCType caseOptionalType(TCOptionalType otype, Context params) { - TCOptionalType otype = (TCOptionalType) type; - return new TCOptionalType(type.location, otype.type.apply(this, params)); + return new TCOptionalType(otype.location, otype.type.apply(this, params)); } @Override - public TCType caseFunctionType(TCFunctionType type, Context params) + public TCType caseFunctionType(TCFunctionType ftype, Context params) { - TCFunctionType ftype = (TCFunctionType) type; - ftype = new TCFunctionType(type.location, instantiate(ftype.parameters, params), ftype.partial, + ftype = new TCFunctionType(ftype.location, instantiate(ftype.parameters, params), ftype.partial, ftype.result.apply(this, params)); ftype.instantiated = true; return ftype; } @Override - public TCType caseParameterType(TCParameterType type, Context params) + public TCType caseParameterType(TCParameterType pname, Context params) { - TCParameterType pname = (TCParameterType) type; Value t = params.lookup(pname.name); if (t == null) @@ -114,31 +110,39 @@ else if (t instanceof ParameterValue) } @Override - public TCType caseProductType(TCProductType type, Context params) + public TCType caseProductType(TCProductType ptype, Context params) { - TCProductType ptype = (TCProductType) type; - return new TCProductType(type.location, instantiate(ptype.types, params)); + return new TCProductType(ptype.location, instantiate(ptype.types, params)); } @Override - public TCType caseSeqType(TCSeqType type, Context params) + public TCType caseSeqType(TCSeqType stype, Context params) { - TCSeqType stype = (TCSeqType) type; - return new TCSeqType(type.location, stype.seqof.apply(this, params)); + return new TCSeqType(stype.location, stype.seqof.apply(this, params)); + } + + @Override + public TCType caseSeq1Type(TCSeq1Type stype, Context params) + { + return new TCSeq1Type(stype.location, stype.seqof.apply(this, params)); + } + + @Override + public TCType caseSetType(TCSetType stype, Context params) + { + return new TCSetType(stype.location, stype.setof.apply(this, params)); } @Override - public TCType caseSetType(TCSetType type, Context params) + public TCType caseSet1Type(TCSet1Type stype, Context params) { - TCSetType stype = (TCSetType) type; - return new TCSetType(type.location, stype.setof.apply(this, params)); + return new TCSet1Type(stype.location, stype.setof.apply(this, params)); } @Override - public TCType caseUnionType(TCUnionType type, Context params) + public TCType caseUnionType(TCUnionType utype, Context params) { - TCUnionType utype = (TCUnionType) type; - return new TCUnionType(type.location, instantiate(utype.types, params)); + return new TCUnionType(utype.location, instantiate(utype.types, params)); } private TCTypeList instantiate(TCTypeList types, Context map) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java index cc74197b7..1705f1525 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/lex/LexTokenReader.java @@ -594,7 +594,6 @@ public LexToken nextToken() throws LexException if (rdCh() == '-') { StringBuilder sb = new StringBuilder(); - LexLocation here = location(linecount, charpos + 1); while (ch != '\n' && ch != EOF) { @@ -602,6 +601,7 @@ public LexToken nextToken() throws LexException rdCh(); } + LexLocation here = new LexLocation(file, currentModule, tokline, tokpos + 2, tokline, lasteol); comments.add(here, sb.toString().substring(1), false); return nextToken(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java index f402199da..22d939741 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java @@ -43,7 +43,6 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.lex.LexTokenReader; import com.fujitsu.vdmj.lex.Token; -import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.messages.ConsoleWriter; import com.fujitsu.vdmj.messages.LocatedException; import com.fujitsu.vdmj.messages.VDMError; @@ -382,7 +381,7 @@ protected ASTAnnotationList readAnnotations(LexCommentList comments) throws LexE { if (Properties.annotations_debug) { - Console.err.println("Annotations: " + e.getMessage() + " at " + comments.location(i)); + warning(5044, "Annotations: " + e.getMessage(), comments.location(i)); } } }