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 4713750461e97b23cef648775a790d889c459622..07a6b3db685524e32e41bbbb04da46ea15aaceb5 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 466f6b4692f962816d89e189976b12ccb4b26f2b..63ea70f5021b7352317af591ff45c2bb745d8256 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 ac0d789c7762064354e84942af9ceb9266312806..14f831f7cbde1436d5f74f211a0871c55665c96a 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 0000000000000000000000000000000000000000..9ffdb5d07ed6c3981ea8524e9ba90c694fa56745 --- /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); + } +}