From 5249fa514a2b71c96ca05d9d3a55a93feda0cba8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe <tlaplus.net@lemmster.de> Date: Fri, 27 Oct 2017 11:57:31 +0200 Subject: [PATCH] The Toolbox generates an MC.tla file upon TLC startup which extends the actual specification being verified. Additionally, to evaluate any constant expression, MC.tla also extends TLC.tla to use the PrintT operator defined in TLC.tla (and its module override tlc2.module.TLC): "ASSUME PrintT(...)" Extending TLC.tla in MC.tla can cause a name clash if the actual specification does *not* extend TLC and happens to declare an operator colliding with one in TLC.tla (e.g. "Permutations", "SortSeq", ...). To resolve this name clash, the Toolbox no longer extends TLC.tla in MC.tla but instead generates a LOCAL declaration of PrintT: "LOCAL PrintT(out) == TRUE ASSUME PrintT(...)" TLC.tla's PrintT is override by the tlc2.module.TLC#PrintT module override. Thus, the LOCAL construct above only resolves the name clash at the SANY level, but produces no output. This class effectively associates MC.tla's PrintT with tlc2.module.TLC#PrintT. The only operator for which this approach obviously does not work is PrintT itself. If the actual specification declares PrintT, evaluating a constant expression will fail. However - contrary to Permutations/SortSeq/... - this is handled gracefully with a proper error message. Fixes Github issue #103 https://github.com/tlaplus/tlaplus/issues/103 [Bug][Toolbox] --- .../toolbox/tool/tlc/model/ModelWriter.java | 2 + .../tla/toolbox/util/ResourceHelper.java | 2 +- .../src/tlc2/module/BuiltInModuleHelper.java | 2 + tlatools/src/tlc2/module/MC.java | 65 +++++++++++++++++++ 4 files changed, 70 insertions(+), 1 deletion(-) create mode 100644 tlatools/src/tlc2/module/MC.java diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java index 471375046..07a6b3db6 100644 --- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java +++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/model/ModelWriter.java @@ -1115,6 +1115,8 @@ public class ModelWriter // value of the constant expression in the TLC output tlaBuffer.append(COMMENT).append("Constant expression ASSUME statement ").append(ATTRIBUTE).append( attributeName).append(CR); + // @see tlc2.module.MC + tlaBuffer.append("LOCAL PrintT(out) == TRUE").append(CR); tlaBuffer.append("ASSUME PrintT(").append(BEGIN_TUPLE).append(CONSTANT_EXPRESSION_EVAL_IDENTIFIER).append( COMMA).append(id).append(END_TUPLE).append(")").append(CR); tlaBuffer.append(SEP).append(CR).append(CR); diff --git a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/ResourceHelper.java b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/ResourceHelper.java index 466f6b469..63ea70f50 100644 --- a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/ResourceHelper.java +++ b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/ResourceHelper.java @@ -776,7 +776,7 @@ public class ResourceHelper { StringBuffer buffer = new StringBuffer(); buffer.append("---- MODULE ").append(ResourceHelper.getModuleNameChecked(moduleFilename, false)).append( - " ----\n").append("EXTENDS ").append(extendedModuleName).append(", TLC").append("\n\n"); + " ----\n").append("EXTENDS ").append(extendedModuleName).append("\n\n"); return buffer; } diff --git a/tlatools/src/tlc2/module/BuiltInModuleHelper.java b/tlatools/src/tlc2/module/BuiltInModuleHelper.java index ac0d789c7..14f831f7c 100644 --- a/tlatools/src/tlc2/module/BuiltInModuleHelper.java +++ b/tlatools/src/tlc2/module/BuiltInModuleHelper.java @@ -58,6 +58,8 @@ public class BuiltInModuleHelper { return true; } else if (clazz == TLC.class && value == TLC.serialVersionUID) { return true; + } else if (clazz == MC.class && value == MC.serialVersionUID) { + return true; } else if (clazz == TransitiveClosure.class && value == TransitiveClosure.serialVersionUID) { return true; } diff --git a/tlatools/src/tlc2/module/MC.java b/tlatools/src/tlc2/module/MC.java new file mode 100644 index 000000000..9ffdb5d07 --- /dev/null +++ b/tlatools/src/tlc2/module/MC.java @@ -0,0 +1,65 @@ +/******************************************************************************* + * Copyright (c) 2017 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.module; + +import tlc2.value.Value; + +/* + * The Toolbox generates an MC.tla file upon TLC startup which extends the actual + * specification being verified. Additionally, to evaluate any constant expression, + * MC.tla also extends TLC.tla to use the PrintT operator defined in TLC.tla + * (and its module override tlc2.module.TLC): + * "ASSUME PrintT(...)" + * + * Extending TLC.tla in MC.tla can cause a name clash if the actual specification + * does *not* extend TLC and happens to declare an operator colliding with one + * in TLC.tla (e.g. "Permutations", "SortSeq", ...). + * + * To resolve this name clash, the Toolbox no longer extends TLC.tla in MC.tla but + * instead generates a LOCAL declaration of PrintT: + * "LOCAL PrintT(out) == TRUE + * ASSUME PrintT(...)" + * + * TLC.tla's PrintT is override by the tlc2.module.TLC#PrintT module override. + * Thus, the LOCAL construct above only resolves the name clash at the SANY level, + * but produces no output. This class effectively associates MC.tla's PrintT with + * tlc2.module.TLC#PrintT. + * + * The only operator for which this approach obviously does not work is PrintT itself. + * If the actual specification declares PrintT, evaluating a constant expression will + * fail. However - contrary to Permutations/SortSeq/... - this is handled gracefully + * with a proper error message. + * + * @see org.lamport.tla.toolbox.tool.tlc.model.ModelWriter.addConstantExpressionEvaluation(String, String) + */ +public class MC { + + public static final long serialVersionUID = 20171027L; + + public static Value PrintT(Value v1) { + return TLC.PrintT(v1); + } +} -- GitLab