A single source of truth instead of multiple copies of TLA+ standard

modules.

[Refactor][Toolbox]

org.lamport.tla.toolbox/.classpath

@@ -3,6 +3,5 @@
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/>
 	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
 	<classpathentry kind="src" path="src"/>
-	<classpathentry exported="true" kind="lib" path="StandardModules" sourcepath="StandardModules"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

org.lamport.tla.toolbox/StandardModules/Bags.tla

------------------------------ MODULE Bags --------------------------------
-(**************************************************************************)
-(* A bag, also called a multiset, is a set that can contain multiple      *)
-(* copies of the same element.  A bag can have infinitely many elements,  *)
-(* but only finitely many copies of any single element.                   *)
-(*                                                                        *)
-(* We represent a bag in the usual way as a function whose range is a     *)
-(* subset of the positive integers.  An element e belongs to bag B iff e  *)
-(* is in the domain of B, in which case bag B contains B[e] copies of e.  *)
-(**************************************************************************)
-EXTENDS TLC
-LOCAL INSTANCE Naturals
-
-IsABag(B) == 
-  (************************************************************************)
-  (* True iff B is a bag.                                                 *)
-  (************************************************************************)
-  B \in [DOMAIN B -> {n \in Nat : n > 0}]
-
-BagToSet(B) == DOMAIN B
-  (************************************************************************)
-  (* The set of elements at least one copy of which is in B.              *)
-  (************************************************************************)
-
-SetToBag(S) == [e \in S |-> 1]  
-  (************************************************************************)
-  (* The bag that contains one copy of every element of the set S.        *)
-  (************************************************************************)
-  
-BagIn(e,B) == e \in BagToSet(B)
-  (************************************************************************)
-  (* The \in operator for bags.                                           *)
-  (************************************************************************)
-
-EmptyBag == SetToBag({})
-
-B1 (+) B2  ==
-  (************************************************************************)
-  (* The union of bags B1 and B2.                                         *)
-  (************************************************************************)
-  [e \in (DOMAIN B1) \cup (DOMAIN B2) |->
-      (IF e \in DOMAIN B1 THEN B1[e] ELSE 0) 
-    + (IF e \in DOMAIN B2 THEN B2[e] ELSE 0) ]
-  
-B1 (-) B2  == 
-  (************************************************************************)
-  (* The bag B1 with the elements of B2 removed--that is, with one copy   *)
-  (* of an element removed from B1 for each copy of the same element in   *)
-  (* B2.  If B2 has at least as many copies of e as B1, then B1 (-) B2    *)
-  (* has no copies of e.                                                  *)
-  (************************************************************************)
-  LET B == [e \in DOMAIN B1 |-> IF e \in DOMAIN B2 THEN B1[e] - B2[e]
-                                                   ELSE B1[e]]
-  IN  [e \in {d \in DOMAIN B : B[d] > 0} |-> B[e]]
-
-LOCAL Sum(f) ==
-        (******************************************************************)
-        (* The sum of f[x] for all x in DOMAIN f.  The definition assumes *)
-        (* that f is a Nat-valued function and that f[x] equals 0 for all *)
-        (* but a finite number of elements x in DOMAIN f.                 *)
-        (******************************************************************)
-        LET DSum[S \in SUBSET DOMAIN f] ==
-               LET elt == CHOOSE e \in S : TRUE
-               IN  IF S = {} THEN 0
-                             ELSE f[elt] + DSum[S \ {elt}]
-        IN  DSum[DOMAIN f]
-
-BagUnion(S) ==
-  (************************************************************************)
-  (* The bag union of all elements of the set S of bags.                  *)
-  (************************************************************************)
-  [e \in UNION {BagToSet(B) : B \in S} |->
-    Sum( [B \in S |-> IF BagIn(e, B) THEN B[e] ELSE 0] ) ]
-
-B1 \sqsubseteq B2  ==
-  (************************************************************************)
-  (* The subset operator for bags.  B1 \sqsubseteq B2 iff, for all e, bag *)
-  (* B2 has at least as many copies of e as bag B1 does.                  *)
-  (************************************************************************)
-  /\ (DOMAIN B1) \subseteq (DOMAIN B2)
-  /\ \A e \in DOMAIN B1 : B1[e] \leq B2[e]
-
-SubBag(B) ==
-  (************************************************************************)
-  (* The set of all subbags of bag B.                                     *)
-  (*                                                                      *)
-  (* The following definition is not the one described in the TLA+ book,  *)
-  (* but rather one that TLC can evaluate.                                *)
-  (************************************************************************)
-
-  LET RemoveFromDom(x, f) == [y \in (DOMAIN f) \ {x} |-> f[y]]
-      Combine(x, BagSet) == 
-         BagSet \cup
-          {[y \in (DOMAIN f) \cup {x} |-> IF y = x THEN i ELSE f[y]] :
-                f \in BagSet, i \in 1..B[x]}
-      Biggest == LET Range == {B[x] : x \in DOMAIN B}
-                 IN  IF Range = {} THEN 0
-                                   ELSE CHOOSE r \in Range :
-                                           \A s \in Range : r \geq s
-      RSB[BB \in UNION {[S -> 1..Biggest] : S \in SUBSET DOMAIN B}] ==
-        IF BB = << >> THEN {<< >>}
-                      ELSE LET x == CHOOSE x \in DOMAIN BB : TRUE
-                           IN  Combine(x, RSB[RemoveFromDom(x, BB)])
-  IN RSB[B]
-
-  (*******************  Here is the definition from the TLA+ book. ********
-  LET AllBagsOfSubset == 
-        (******************************************************************)
-        (* The set of all bags SB such that BagToSet(SB) \subseteq        *)
-        (* BagToSet(B).                                                   *)
-        (******************************************************************)
-        UNION {[SB -> {n \in Nat : n > 0}] : SB \in SUBSET BagToSet(B)}  
-  IN  {SB \in AllBagsOfSubset : \A e \in DOMAIN SB : SB[e] \leq B[e]}
-  ***************************************************************************)
-
-BagOfAll(F(_), B) ==
-  (************************************************************************)
-  (* The bag analog of the set {F(x) : x \in B} for a set B. It's the bag *)
-  (* that contains, for each element e of B, one copy of F(e) for every   *)
-  (* copy of e in B. This defines a bag iff, for any value v, the set of  *)
-  (* e in B such that F(e) = v is finite.                                 *)
-  (************************************************************************)
-  [e \in {F(d) : d \in BagToSet(B)} |-> 
-     Sum( [d \in BagToSet(B) |-> IF F(d) = e THEN B[d] ELSE 0] ) ]
-
-BagCardinality(B) ==
-  (************************************************************************)
-  (* If B is a finite bag (one such that BagToSet(B) is a finite set),    *)
-  (* then this is its cardinality (the total number of copies of elements *)
-  (* in B).  Its value is unspecified if B is infinite.                   *)
-  (************************************************************************)
-  Sum(B)
-
-CopiesIn(e, B) ==
-  (************************************************************************)
-  (* If B is a bag, then CopiesIn(e, B) is the number of copies of e in   *)
-  (* B. If ~BagIn(e, B), then CopiesIn(e, B) = 0.                         *)
-  (************************************************************************)
-  IF BagIn(e, B) THEN B[e] ELSE 0
-=============================================================================
-
-(* Last modified on Fri 26 Jan 2007 at  8:45:03 PST by lamport *)
-
- 6 Apr 99 : Modified version for standard module set
- 7 Dec 98 : Corrected error found by Stephan Merz.
- 6 Dec 98 : Modified comments based on suggestions by Lyle Ramshaw.
- 5 Dec 98 : Initial version.

org.lamport.tla.toolbox/StandardModules/FiniteSets.tla

----------------------------- MODULE FiniteSets -----------------------------
-LOCAL INSTANCE Naturals
-LOCAL INSTANCE Sequences
-  (*************************************************************************)
-  (* Imports the definitions from Naturals and Sequences, but doesn't      *)
-  (* export them.                                                          *)
-  (*************************************************************************)
-
-IsFiniteSet(S) == 
-  (*************************************************************************)
-  (* A set S is finite iff there is a finite sequence containing all its   *)
-  (* elements.                                                             *)
-  (*************************************************************************)
-  \E seq \in Seq(S) : \A s \in S : \E n \in 1..Len(seq) : seq[n] = s
-
-Cardinality(S) ==
-  (*************************************************************************)
-  (* Cardinality is defined only for finite sets.                          *)
-  (*************************************************************************)
-  LET CS[T \in SUBSET S] == IF T = {} THEN 0
-                                      ELSE 1 + CS[T \ {CHOOSE x : x \in T}]
-  IN  CS[S]
-=============================================================================

org.lamport.tla.toolbox/StandardModules/Integers.tla

--------------------------------- MODULE Integers ----------------------------
-(***************************************************************************)
-(* A dummy module that declares the operators that are defined in the      *)
-(* real Integers module.                                                   *)
-(***************************************************************************)
-EXTENDS Naturals
-
-Int  ==  { }
--. a == 0 - a
-=============================================================================

org.lamport.tla.toolbox/StandardModules/Naturals.tla

--------------------------------- MODULE Naturals ----------------------------
-(***************************************************************************)
-(* A dummy module that defines the operators that are defined by the       *)
-(* real Naturals module.                                                   *)
-(***************************************************************************)
-
-Nat       == { }
-a+b       == {a, b}
-a-b       == {a, b}
-a*b       == {a, b}
-a^b       == {a, b}
-a<b       ==  a = b
-a>b       ==  a = b
-a \leq b  ==  a = b
-a \geq b  ==  a = b
-a % b     ==  {a, b}
-a \div b  ==  {a, b}
-a .. b    ==  {a, b}
-=============================================================================

org.lamport.tla.toolbox/StandardModules/RealTime.tla

------------------------------ MODULE RealTime -------------------------------
-EXTENDS Reals 
-VARIABLE now
-
-RTBound(A, v, D, E) == 
-  LET TNext(t)  ==  t' = IF <<A>>_v \/ ~(ENABLED <<A>>_v)'
-                           THEN 0 
-                           ELSE t + (now'-now)
-
-      Timer(t) == (t=0)  /\  [][TNext(t)]_<<t, v, now>>
-
-      MaxTime(t) == [](t \leq E) 
-
-      MinTime(t) == [][A => t \geq D]_v 
-  IN \EE t : Timer(t) /\ MaxTime(t) /\ MinTime(t)
------------------------------------------------------------------------------
-RTnow(v) == LET NowNext == /\ now' \in {r \in Real : r > now} 
-                           /\ UNCHANGED v
-            IN  /\ now \in Real 
-                /\ [][NowNext]_now
-                /\ \A r \in Real : WF_now(NowNext /\ (now'>r))
-=============================================================================

org.lamport.tla.toolbox/StandardModules/Reals.tla

--------------------------------- MODULE Reals -------------------------------
-(***************************************************************************)
-(* A dummy module that declares the operators that are defined in the      *)
-(* real Reals module.  It should produce an error if TLC tries to          *)
-(* evaluate these operators when it shouldn't.                             *)
-(***************************************************************************)
-EXTENDS Integers
-
-Real  ==  "Reals"
-a / b == CHOOSE m \in Real : m * b = a
-Infinity == CHOOSE i : (i \notin Real) /\ (\A r \in Real : i > r)
-=============================================================================

org.lamport.tla.toolbox/StandardModules/Sequences.tla

------------------------------- MODULE Sequences -----------------------------
-(***************************************************************************)
-(* Defines operators on finite sequences, where a sequence of length n is  *)
-(* represented as a function whose domain is the set 1..n (the set         *)
-(* {1, 2, ... , n}).  This is also how TLA+ defines an n-tuple, so         *)
-(* tuples are sequences.                                                   *)
-(***************************************************************************)
-
-LOCAL INSTANCE Naturals
-  (*************************************************************************)
-  (* Imports the definitions from Naturals, but don't export them.         *)
-  (*************************************************************************)
-  
-Seq(S) == UNION {[1..n -> S] : n \in Nat}
-  (*************************************************************************)
-  (* The set of all sequences of elements in S.                            *)
-  (*************************************************************************)
-
-Len(s) == CHOOSE n \in Nat : DOMAIN s = 1..n
-  (*************************************************************************)
-  (* The length of sequence s.                                             *)
-  (*************************************************************************)
-
-s \o t == [i \in 1..(Len(s) + Len(t)) |-> IF i \leq Len(s) THEN s[i]
-                                                           ELSE t[i-Len(s)]]
-  (*************************************************************************)
-  (* The sequence obtained by concatenating sequences s and t.             *)
-  (*************************************************************************)
-
-Append(s, e) == s \o <<e>>
-  (**************************************************************************)
-  (* The sequence obtained by appending element e to the end of sequence s. *)
-  (**************************************************************************)
-
-Head(s) == s[1]
-Tail(s) == CASE s # << >> -> [i \in 1..(Len(s)-1) |-> s[i+1]]
-  (*************************************************************************)
-  (* The usual head (first) and tail (rest) operators. (Definition of Tail *)
-  (* changed on 4 Jun 2013 because original defined Tail(<< >>) = << >> .  *)
-  (*************************************************************************)
-
-SubSeq(s, m, n) == [i \in 1..(1+n-m) |-> s[i+m-1]]
-  (*************************************************************************)
-  (* The sequence <<s[m], s[m+1], ... , s[n]>>.                            *)
-  (*************************************************************************)
-  
-SelectSeq(s, Test(_)) == 
-  (*************************************************************************)
-  (* The subsequence of s consisting of all elements s[i] such that        *)
-  (* Test(s[i]) is true.                                                   *)
-  (*************************************************************************)
-  LET F[i \in 0..Len(s)] == 
-        (*******************************************************************)
-        (* F[i] equals SelectSeq(SubSeq(s, 1, i), Test]                    *)
-        (*******************************************************************)
-        IF i = 0 THEN << >>
-                 ELSE IF Test(s[i]) THEN Append(F[i-1], s[i])
-                                    ELSE F[i-1]
-  IN F[Len(s)]
-=============================================================================

org.lamport.tla.toolbox/StandardModules/TLC.tla

-------------------------------- MODULE TLC ----------------------------------
-LOCAL INSTANCE Naturals
-LOCAL INSTANCE Sequences
------------------------------------------------------------------------------
-Print(out, val) == val
-PrintT(out) == TRUE
-Assert(val, out) == IF val = TRUE THEN TRUE
-                                  ELSE CHOOSE v : TRUE
-JavaTime == CHOOSE n : n \in Nat
-TLCGet(i) == CHOOSE n : TRUE
-TLCSet(i, v) == TRUE
------------------------------------------------------------------------------
-d :> e == [x \in {d} |-> e]
-f @@ g == [x \in (DOMAIN f) \cup (DOMAIN g) |->
-            IF x \in DOMAIN f THEN f[x] ELSE g[x]]
-Permutations(S) == 
-   {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}
------------------------------------------------------------------------------
-(***************************************************************************)
-(* In the following definition, we use Op as the formal parameter rather   *)
-(* than \prec because TLC Version 1 can't handle infix formal parameters.  *)
-(***************************************************************************)
-SortSeq(s, Op(_, _)) ==
-    LET Perm == CHOOSE p \in Permutations(1 .. Len(s)) :
-                  \A i, j \in 1..Len(s) : 
-                     (i < j) => Op(s[p[i]], s[p[j]]) \/ (s[p[i]] = s[p[j]])
-    IN  [i \in 1..Len(s) |-> s[Perm[i]]]
-
-RandomElement(s) == CHOOSE x \in s : TRUE
-
-Any == CHOOSE x : TRUE
-
-ToString(v) == (CHOOSE x \in [a : v, b : STRING] : TRUE).b
-
-TLCEval(v) == v
-=============================================================================

org.lamport.tla.toolbox/build.properties

@@ -4,8 +4,6 @@ bin.includes = plugin.xml,\
                META-INF/,\
                .,\
                icons/,\
-               StandardModules/,\
                helpContexts.xml,\
                images/
-jars.compile.order = .,\
-                     StandardModules/
+jars.compile.order = .

org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/spec/Module.java

@@ -29,9 +29,9 @@ package org.lamport.tla.toolbox.spec;
 import java.io.File;
 
 import org.eclipse.core.resources.IResource;
-import org.lamport.tla.toolbox.util.RCPNameToFileIStream;
 
 import tla2sany.semantic.ModuleNode;
+import tlc2.module.BuiltInModuleHelper;
 
 /**
  * Representation of a module
@@ -128,11 +128,11 @@ public class Module
      * Determines if current module is a standard module <br>
      * TODO Fishy method. improve/unify it
      * 
-     * @return true iff the absolute path of the module contains RCPNameToFileIStream.STANDARD_MODULES value
+     * @return true iff the absolute path of the module contains BuiltInModuleHelper.STANDARD_MODULES value
      */
     public boolean isStandardModule()
     {
-        return (getAbsolutePath().indexOf(RCPNameToFileIStream.STANDARD_MODULES) != -1);
+        return (getAbsolutePath().indexOf(BuiltInModuleHelper.STANDARD_MODULES) != -1);
     }
 
     

org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/util/RCPNameToFileIStream.java

@@ -7,9 +7,11 @@ import java.util.Enumeration;
 import java.util.Vector;
 
 import org.eclipse.core.runtime.FileLocator;
-import org.lamport.tla.toolbox.Activator;
+import org.eclipse.core.runtime.Platform;
+import org.osgi.framework.Bundle;
 
 import tla2sany.semantic.ModuleNode;
+import tlc2.module.BuiltInModuleHelper;
 import util.FilenameToStream;
 import util.ToolIO;
 
@@ -21,9 +23,7 @@ import util.ToolIO;
 public class RCPNameToFileIStream implements FilenameToStream
 {
 
-    // TODO move to generic constant interface
-    public static final String STANDARD_MODULES   = "StandardModules";
-    private Vector             libraryPathEntries = new Vector();
+    private final Vector<String> libraryPathEntries = new Vector<String>();
 
     /**
      * Initialization of the name resolver <br>
@@ -56,22 +56,31 @@ public class RCPNameToFileIStream implements FilenameToStream
     {
         try
         {
-            Enumeration installedInternalModules = Activator.getDefault().getBundle().findEntries(File.separator,
-                    STANDARD_MODULES, true);
-            Vector paths = new Vector();
+        	final Bundle bundle = Platform.getBundle(BuiltInModuleHelper.BUNDLE_ID);
+        	
+			Enumeration<URL> installedInternalModules = bundle
+					.findEntries(BuiltInModuleHelper.STANDARD_MODULES_PATH, BuiltInModuleHelper.STANDARD_MODULES, true);
+			
+			if (installedInternalModules == null) {
+				// Toolbox is running from inside Eclipse (dev mode) and the StandardModules are
+				// found in a slightly different location.
+				installedInternalModules = bundle.findEntries(
+						File.separator + "src" + File.separator + BuiltInModuleHelper.STANDARD_MODULES_PATH,
+						BuiltInModuleHelper.STANDARD_MODULES, true);
+			}
+			
             while (installedInternalModules.hasMoreElements())
             {
-                URL library = (URL) installedInternalModules.nextElement();
+                final URL library = installedInternalModules.nextElement();
                 if (library != null)
                 {
                     // add external (resolved) URL
-                    paths.addElement(FileLocator.resolve(library).getPath());
+                	final String path = FileLocator.resolve(library).getPath();
+                	libraryPathEntries.add(path);
                 }
             }
-            libraryPathEntries.addAll(paths);
         } catch (IOException e)
         {
-            // TODO Auto-generated catch block
             e.printStackTrace();
         }
 

tlatools/src/tlc2/module/BuiltInModuleHelper.java

@@ -26,10 +26,16 @@
 
 package tlc2.module;
 
+import java.io.File;
 import java.lang.reflect.Field;
 
 public class BuiltInModuleHelper {
 	
+	public static final String BUNDLE_ID = "org.lamport.tlatools";
+
+	public static final String STANDARD_MODULES = "StandardModules";
+	public static final String STANDARD_MODULES_PATH = File.separator + "tla2sany" + File.separator;
+	
 	private BuiltInModuleHelper() {
 		// no instantiation
 	}