diff --git a/general/docs/changelogs/ch1_7_1.md b/general/docs/changelogs/ch1_7_1.md index 45b386f90a9d91304c72122e72fa8bc1f1e15c80..5d897104801dab36577e7a47fa276cab49d0c175 100644 --- a/general/docs/changelogs/ch1_7_1.md +++ b/general/docs/changelogs/ch1_7_1.md @@ -3,27 +3,19 @@ The high level changelog is available at http://research.microsoft.com/en-us/um/ ### Additional _noteworthy_ changes -#### Tools - -##### Bugfix -* TLC shows no error *trace* for violations of `TLC!Assert`, ... (regression in 1.7.0) https://github.com/tlaplus/tlaplus/issues/461 +* TLC shows no error *trace* for violations of `TLC!Assert`, ... https://github.com/tlaplus/tlaplus/issues/461 * NoClassDefError when running TLC on Java 1.8. https://github.com/tlaplus/tlaplus/issues/462 * Dot visualization (graphviz) fails due to invalid character ! when spec uses instantiation https://github.com/tlaplus/tlaplus/issues/452 * Simulation mode ignores ASSUMPTIONS. https://github.com/tlaplus/tlaplus/issues/496 * Back to state missing for lasso error trace found by simulation https://github.com/tlaplus/tlaplus/issues/497 * AtNode does not show up in (dot) graph output of semantic explorer 52f3b01 * Replace custom implementation of (heap) sort in TeX with java.utils.Arrays#sort https://github.com/tlaplus/tlaplus/issues/539 -End support for liveness checking and multiple workers in DFID mode because both features are unreliable https://github.com/tlaplus/tlaplus/issues/548 https://github.com/tlaplus/tlaplus/issues/544 - -#### Toolbox - -##### Bugfix +* End support for liveness checking and multiple workers in DFID mode because both features are unreliable https://github.com/tlaplus/tlaplus/issues/548 https://github.com/tlaplus/tlaplus/issues/544 * Multiline trace expressions fail to parse in Toolbox. defe0c74915b1c27c6af2fb55c8163f3574c8918 * Re-worked PlusCal/TLA+ divergence warning (please manually remove [1.7.0 markers](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.0)). f1cf514c3b334b0968a5ac7fdf14d3e93905b14c e434e139adebf73ed8f9470117031f1ad4b749df 7c61d1a70f03fe4e54142f59487af90745386b74 * Upgrade Eclipse foundation to its 2020-06 release for better HiDPI support. https://github.com/tlaplus/tlaplus/issues/472 * Toolbox intermittently shows no error trace on an invariant violation https://github.com/tlaplus/tlaplus/issues/538 - ### Checksums sha1sum|file ------------ | ------------- diff --git a/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java index 22de7b25fba05f028e88a78dc3270dbfa8322ffe..51be055c814bf01e5d2a60033e494c3e902295e3 100644 --- a/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java +++ b/tlatools/org.lamport.tlatools/src/pcal/PcalParams.java @@ -18,8 +18,13 @@ public final class PcalParams /** * Parameters to be updated on each new release. */ - public static final String modDate = "10 July 2019"; - public static final String version = "1.9"; + public static final String modDate = "31 December 2020"; + // Can't increment 1.9 to 1.10 because VersionToNumber(str) calculates a lower + // numerical value for 1.10 than it does for 1.9. This breaks the FairSeq?Test + // tests. Until we switch from 1.xx to 2.0, increment versionWeight along with + // version. + public static final int versionWeight = 1902; + public static final String version = "1.11"; /** * SZ Mar 9, 2009: * Added re-initialization method. Since PcalParams class @@ -50,7 +55,7 @@ public final class PcalParams NoDoneDisjunct = false; optionsInFile = false; versionOption = null; - inputVersionNumber = VersionToNumber(PcalParams.version); + inputVersionNumber = PcalParams.versionWeight; PcalTLAGen.wrapColumn = 78; PcalTLAGen.ssWrapColumn = 45; tlaPcalMapping = null ; @@ -247,7 +252,7 @@ public final class PcalParams // way because of the way the code evolved, and no intelligent // design has stepped in to fix it. public static String versionOption = null; - public static int inputVersionNumber = VersionToNumber(PcalParams.version); + public static int inputVersionNumber = PcalParams.versionWeight; // The input file's version number * 1000 // public static boolean readOnly = false; // True iff this is a .pcal input file and the .tla file should @@ -310,7 +315,7 @@ public final class PcalParams PcalDebug.reportError("Illegal version " + ver + " specified."); return false; } - if (vnum > VersionToNumber(PcalParams.version)) { + if (vnum > PcalParams.versionWeight) { PcalDebug.reportError("Specified version " + ver + " later than current version " + PcalParams.version); return false; diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java index e6aee0b5c60b17f2d671a4038194dada25ccfe68..d68116ed66325a1ca4b4f3f87dd6fd430cc0af2e 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java @@ -23,7 +23,7 @@ public class TLCGlobals public static final int DEFAULT_CHECKPOINT_DURATION = (30 * 60 * 1000) + 42; // The current version of TLC - public static String versionOfTLC = "Version 2.15 of Day Month 20??"; + public static String versionOfTLC = "Version 2.16 of 31 December 2020"; // The bound for set enumeration, used for pretty printing public static int enumBound = 2000; diff --git a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product index 504bf73169c829504693b28d532f1ee34fa43a82..e79ef3fa9372269920d06b4d75113bffcb817287 100644 --- a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product +++ b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product @@ -8,10 +8,10 @@ <text> TLA+ Toolbox provides a user interface for TLA+ Tools. -This is Version 1.7.1 of Day Month Year and includes: +This is Version 1.7.1 of 31 December 2020 and includes: - SANY Version 2.2 of 20 April 2020 - - TLC Version 2.15 of 20 April 2020 - - PlusCal Version 1.10 of 20 April 2020 + - TLC Version 2.16 of 31 December 2020 + - PlusCal Version 1.11 of 31 December 2020 - TLATeX Version 1.0 of 20 September 2017 Don't forget to click on help. You can learn about features that you never knew about or have forgotten. diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml index 620d83498e6f4fc84f2e5123b4c5aa9389f97f68..98d54a174ed9411d1a92667eccad0a4f5fac20ed 100644 --- a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml +++ b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml @@ -30,7 +30,7 @@ </property> <property name="aboutText" - value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.1 of Day Month Year and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.15 of 20 April 2020
 - PlusCal Version 1.10 of 20 April 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com"> + value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.7.1 of 31 December 2020 and includes:
 - SANY Version 2.2 of 20 April 2020
 - TLC Version 2.16 of 31 December 2020
 - PlusCal Version 1.11 of 31 December 2020
 - TLATeX Version 1.0 of 20 September 2017

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .

Some icons used in the Toolbox were provided by www.flaticon.com"> </property> <property name="aboutImage" diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java index 5467a41bb289c4263865f63fe1179b29416b36ee..8a8e21c454c87eed26cb8338f85c680c91538165 100644 --- a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java +++ b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java @@ -431,7 +431,7 @@ public class ToolboxIntroPart extends IntroPart implements IIntroPart { final Label lblVersion = new Label(outerContainer, SWT.WRAP); lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1)); - lblVersion.setText("Version 1.7.1 of Day Month Year"); + lblVersion.setText("Version 1.7.1 of 31 December 2020"); lblVersion.setBackground(backgroundColor); }