Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • master
  • towards_1.8.0
  • updateTLC
  • 1.0.0-stups
  • 1.0.1-stups
  • 1.0.2-stups
  • 1.1.0-stups
7 results

Target

Select target project
No results found
Select Git revision
  • master
  • towards_1.8.0
  • updateTLC
  • 1.0.0-stups
  • 1.0.1-stups
  • 1.0.2-stups
  • 1.1.0-stups
7 results
Show changes

Commits on Source 242

142 additional commits have been omitted to prevent performance issues.
674 files
+ 57240
− 16231
Compare changes
  • Side-by-side
  • Inline

Files

.gitignore

+3 −0
Original line number Diff line number Diff line
@@ -29,3 +29,6 @@ tlatools/build 
!**/gradle/wrapper/gradle-wrapper.jar

ajcore.*.txt

tlatools/test-model/CodePlexBug08/checkpoint/

tlatools/test-model/CallGotoUnlabeledTest.old

junit[0-9]*.properties

junitvmwatcher[0-9]*.properties

CONTRIBUTING.md

+3 −1
Original line number Diff line number Diff line 
We welcome contributions from volunteers. A number of [improvements we'd like to see implemented](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) are listed at [general/docs/contributions.md](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) in addition to the [issues tagged with "helpwanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). But we're happy to consider anything you'd like to contribute. However, some parts of the tlaplus repository follow a very strict contribution policy. So before you start working on anything, please [discuss with us](https://github.com/tlaplus/tlaplus/issues) what you want to do. You can do that on the [issues page](https://github.com/tlaplus/tlaplus/issues). We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.

Is this your first contribution to Open Source? If yes, please read the excellent first time contributor guide at [https://opensource.guide/how-to-contribute/](https://opensource.guide/how-to-contribute/).



Generally, we welcome contributions from volunteers. A number of [improvements we'd like to see implemented](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) are listed at [general/docs/contributions.md](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) in addition to the [issues tagged with "helpwanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). But we're happy to consider anything you'd like to contribute. However, some parts of the tlaplus repository follow a very strict contribution policy. So before you start working on anything, please [discuss with us](https://github.com/tlaplus/tlaplus/issues) what you want to do. You can do that on the [issues page](https://github.com/tlaplus/tlaplus/issues). We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.

general/docs/changelogs/ch1_5_7.md

0 → 100644
+46 −0
Original line number Diff line number Diff line 
### Changelog

The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.5.7 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.5.7+is%3Aclosed) lists all completed issues.



### Additional noteworthy changes



#### TLC

* Reword and complete comments of TLA<sup>+</sup> standard modules d2f54a1a5e3b7d9a9ac397046e147c7ef63c2f9d

* IsABag inconsistent with Bags.tla when parameter is not a bag 5d15bde33891d34cdf07eaaf94845db665c59c72

* BagsUnion operator of TLA<sup>+</sup> standard module for `BagUnion({b,b})` produces incorrect `b (+) b` as result bc0f7dbf89a703a5899689b98232f1fe02241918

* [Correctly handle sequences as input to Bags operators](https://github.com/tlaplus/tlaplus/issues/139)

* [Provisional Randomization standard module]

* tlc2.Generator refactored into tlc2.TLC 6141aed0c680f6b3257527e91d6652fc5adedaa6

* Correctly recreate error trace in BFS mode with RandomElement 3a618d7dc566dd1fbae90d2ebbe5066d2c300fe2

* Minimize the number of duplicate states that are generated as part of the initial predicate f3a98cec010b63a4d0fb6fa122e6bd4e675ff3ae

* Minimize the number of duplicate states that are generated as part of the next-state predicate fba43190b2aa1ab58fecbddd1b878aaad0d3de1a

* Indicate name of action which does not completely specified the successor state fddcdd48b8d7ab402be887d484a2d6d2198cdb56

* Speed-up Cloud TLC by skipping instance provisioning 2bc248848d89b094b74810c808f50eaa04506ddd

* Colorize and label actions (arcs) in state graph visualization 7e80f1d6301c42c5381ef63c2ed26166c35f12bc ([Screenshot](https://user-images.githubusercontent.com/6131840/35131485-64933ddc-fc94-11e7-9b71-04f543877abe.png)) Contributor: [will62794](https://github.com/will62794)

* Fix broken error traces with views 5a629454ed5286076f5f6012b382e852448d165c



#### PlusCal

* Allow no intervening label between call and goto in PlusCal 188e1fd65788f5499030da53b6481351d4564b8c



#### Specification Editor

* Show errors in PlusCal algorithm for assignments to undeclared variables 1e3f8fae00d12e5d1e755ad47e95dacaaa5c46af

* Editor command "Goto declaration" now also goes to declarations of TLA+ standard modules 103204a62dabae2e68b8f728a11af50a64205dcf ([Screencast](https://user-images.githubusercontent.com/88777/42322087-a7e0946a-804a-11e8-9ee7-fa4be54aa7b2.gif))

* Mouse hover help shows BNF and help for PlusCal statements dbeafb64c395c6bd936a1bf0026c5780032e34ed

* Show operation definition and comment in mouse hover help ad36f390a22f24ebef23cd3d387e3a371fb90c2b

* Code completion for PlusCal statements triggered by Ctrl+Space 13c772ff44b494d00a9dc95d429c5ec7cfb0e494 ([Screencast](https://user-images.githubusercontent.com/88777/42321184-930decf2-8047-11e8-9f92-2447695504f8.gif))

* Code completion for operator definitions and declarations triggered by Ctrl+Space c31c2bd2b6ed9cf66dc733b7e39639b8837a516f ([Screencast](https://user-images.githubusercontent.com/88777/42320885-7b2a4ef6-8046-11e8-846d-5f9340c445fe.gif))

* Automatically transpile PlusCal to TLA+ on editor save 642b540e0d479867ec73c202795106ed5ed9454a ([Screencast](https://user-images.githubusercontent.com/88777/42319531-cc8d9afa-8041-11e8-91e9-3b4656243e4f.gif))



#### Model Editor

* Collapse, disable and annotate "Generals" and "Statistics" sections with "No behavior spec" 43d207d0b3368401900a927ffea790ce041bde55

* Add undo and redo support to constant expression source viewer ff03c664b0ed4bf435df216c3b6fec758a3b95be

* Add TLA+ syntax highlighting to constant expression source viewer fd93b56ced23a1e15c1e2f24ad67303c88a0cb09

* Report the number of initial states as first item reported in the ResultPage's statistic table (with diameter of 0) 076f0c78635fe29ff1cfd6c68f3109fb6f04b191

* Show output/progress of remotely running Cloud TLC in Toolbox 593fc822e89d84ffbb586a3a73f0d143af502f1d



#### Misc

* [Add a mechanism to inform Toolbox users about important news](https://github.com/tlaplus/tlaplus/issues/100) ([Screencast](https://user-images.githubusercontent.com/88777/42326534-f1987984-8058-11e8-8dfb-afe2333d9ff2.gif)) Contributor: [quaeler](https://github.com/quaeler)

* Update Eclipse Foundation to Oxygen SR3 ed931d03fe4e33135f80f5957b0d2d76f815ab7f



### 32 bits

32 bit (x86) variants of the TLA Toolbox have been discontinued with this release. fb680446557e92229a059ef9f93fd48a29c5bb2f

general/docs/changelogs/gh-1_5_7.jq

0 → 100644
+7 −0
Original line number Diff line number Diff line 
{

  "tag_name": "v1.5.6",

  "name": "The Xenophon release",

  "draft": true,

  "prerelease": false,

  "body": $changelog

}
 
 No newline at end of file

general/docs/contributions.md

+1 −4
Original line number Diff line number Diff line
@@ -6,7 +6,7 @@ Please also consult the [issues tracker](https://github.com/tlaplus/tlaplus/issu 
TLC model checker

-----------------

#### Concurrent search for strongly connected components (difficulty: high) (skills: Java, TLA+)

One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and [studied in the scope of other model checkers](https://github.com/utwente-fmt/ppopp16). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.

One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and studied in the scope of other model checkers ([Multi-Core On-The-Fly SCC Decomposition](https://github.com/utwente-fmt/ppopp16) & [Concurrent On-the-Fly SCC Detection for Automata-Based Model Checking with Fairness Assumption](http://ieeexplore.ieee.org/document/7816578/)). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.



#### Liveness checking under symmetry (difficulty: high) (skills: Java, TLA+)

[Symmetry reduction](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Symmetry%20Reductions%20in%20Model%20Checking.pdf) techniques can significantly reduce the size of the state graph generated and checked by TLC. For safety checking, symmetry reduction is well studied and has long been implemented in TLC. TLC's liveness checking procedure however, can fail to find property violations if symmetry is declared. Yet, there is no reason why symmetry reduction cannot be applied to liveness checking. This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
@@ -45,9 +45,6 @@ TLA Toolbox 
#### Port Toolbox to e4 (difficulty: easy) (skills: Java, Eclipse)

[e4](http://www.vogella.com/tutorials/EclipseRCP/article.html) represents the newest programming model for Eclipse RCP applications. e4 provides higher flexibility while simultaneously reducing boilerplate code. The TLA Toolbox has been implemented on top of Eclipse RCP 3.x and thus is more complex than it has to.



#### Package Toolbox for Debian and Fedora based Linux distributions (difficulty: easy) (skills: Eclipse, Linux)

The current Toolbox installation requires Linux users to download a zip file, to extract it and manually integrate the Toolbox into the System. Packaging the Toolbox for Debian (.deb) and Fedora (.rpm) based Linux distributions would not only simplify the installation procedure, it would also create more visible for TLA+ within the Linux community.



#### Add support for Google Compute to Cloud TLC (difficulty: easy) (skills: jclouds, Linux)

The Toolbox can launch Azure and Amazon EC2 instances to run model checking in the cloud. The Toolbox interfaces with clouds via the [jclouds](https://jclouds.apache.org/) toolkit. jclouds has support for Google Compute, but https://github.com/tlaplus/tlaplus/blob/master/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java has to be enhanced to support Google Compute.

general/performance/Ghostferry/MC.cfg

0 → 100644
+43 −0
Original line number Diff line number Diff line 
\* MV CONSTANT declarations

CONSTANTS

r0 = r0

r1 = r1

r2 = r2

\* CONSTANT declarations

CONSTANT defaultInitValue = defaultInitValue

\* MV CONSTANT definitions

CONSTANT

Records <- const_152748923762611000

\* CONSTANT declarations

CONSTANT Ferry = Ferry

\* CONSTANT declarations

CONSTANT Application = Application

\* CONSTANT declarations

CONSTANT BinlogStreamer = BinlogStreamer

\* CONSTANT declarations

CONSTANT TableIterator = TableIterator

\* CONSTANT definitions

CONSTANT

MaxPrimaryKey <- const_152748923762612000

\* CONSTANT definitions

CONSTANT

InitialTable <- const_152748923762613000

\* CONSTANT definitions

CONSTANT

MaxBinlogSize <- const_152748923762614000

\* CONSTANT definition

CONSTANT

NoRecordHere = NoRecordHere

\* ACTION_CONSTRAINT definition

ACTION_CONSTRAINT

action_constr_152748923762616000

\* SPECIFICATION definition

SPECIFICATION

spec_152748923762617000

\* INVARIANT definition

INVARIANT

inv_152748923762618000

\* PROPERTY definition

PROPERTY

prop_152748923762619000

\* Generated on Mon May 28 08:33:57 CEST 2018
 
 No newline at end of file

general/performance/Ghostferry/MC.tla

0 → 100644
+47 −0
Original line number Diff line number Diff line 
---- MODULE MC ----

EXTENDS ghostferry, TLC



\* MV CONSTANT declarations@modelParameterConstants

CONSTANTS

r0, r1, r2

----



\* MV CONSTANT definitions Records

const_152748923762611000 == 

{r0, r1, r2}

----



\* CONSTANT definitions @modelParameterConstants:2MaxPrimaryKey

const_152748923762612000 == 

3

----



\* CONSTANT definitions @modelParameterConstants:4InitialTable

const_152748923762613000 == 

<<r0, r1, r2, NoRecordHere>>

----



\* CONSTANT definitions @modelParameterConstants:8MaxBinlogSize

const_152748923762614000 == 

4

----



\* ACTION_CONSTRAINT definition @modelParameterActionConstraint:0

action_constr_152748923762616000 ==

BinlogSizeActionConstraint

----

\* SPECIFICATION definition @modelBehaviorSpec:0

spec_152748923762617000 ==

Spec

----

\* INVARIANT definition @modelCorrectnessInvariants:0

inv_152748923762618000 ==

SourceTargetEquality

----

\* PROPERTY definition @modelCorrectnessProperties:0

prop_152748923762619000 ==

Termination

----

=============================================================================

\* Modification History

\* Created Mon May 28 08:33:57 CEST 2018 by markus

general/performance/Ghostferry/README.md

0 → 100644
+1 −0
Original line number Diff line number Diff line 
# This is a snapshot of the tlaplus folder of the repository at https://github.com/Shopify/ghostferry/ - released under the MIT license - from which we copied the spec for TLC performance testing! We claim no authorship of this specification.

general/performance/Grid5k/Grid5k.tla

0 → 100644
+32 −0
Original line number Diff line number Diff line 
-------------------------------- MODULE Grid5k --------------------------------

\* This spec executes

\*  variable x = [i \in 1..N |-> 0];

\*  while (TRUE) {

\*    with (i \in 1..N) {

\*        x[i] := (x[i] + 1) % K ;

\*        \* SUBSET 1..L causes TLC to generate the power set of the set 1..L.

\*        \* For each set in the power set, TLC evaluates if the set's 

\*        \* cardinality is L... KaBOOM!

\*        await \E s \in SUBSET (1..L): Cardinality(s) = L

\*        }

\*   }

\*  Thus,  - N is the number of states computed for each evaluation of the

\*           next-state action

\*         - K^N is the total number of distinct states

\*         - The time to compute a single state is asymptotically

\*           proportional to 2^L.

\*         - C defines the number of initial states. Let C=n

\*           then the state graph has n isomorphic disjunct subgraphs.

EXTENDS Integers, FiniteSets



CONSTANTS N, K, L, C

VARIABLE x, y



Init == /\ x = [i \in 1..N |-> 0]

        /\ y \in 1..C



Next == /\ UNCHANGED y

        /\ \E i \in 1..N : /\ x' = [x EXCEPT ![i] = (@ + 1) % K]

        /\ \E s \in SUBSET (1..L): Cardinality(s) = L



=============================================================================

general/performance/Grid5k/MC.cfg

0 → 100644
+7 −0
Original line number Diff line number Diff line 
CONSTANT K=05

CONSTANT L=01

CONSTANT N=10

CONSTANT C=32

INIT Init

NEXT Next

general/performance/Grid5k/MC.tla

0 → 100644
+4 −0
Original line number Diff line number Diff line 
-------- MODULE MC ---------

EXTENDS Grid5k

===================

general/performance/MongoRepl/MC.cfg

0 → 100644
+33 −0
Original line number Diff line number Diff line 
\* MV CONSTANT declarations

CONSTANTS

v1 = v1

\* MV CONSTANT declarations

CONSTANTS

s1 = s1

s2 = s2

s3 = s3

\* CONSTANT declarations

CONSTANT Nil = Nil

\* CONSTANT declarations

CONSTANT Follower = Follower

\* MV CONSTANT definitions

CONSTANT

Value <- const_1518107340940126000

\* CONSTANT declarations

CONSTANT Leader = Leader

\* MV CONSTANT definitions

CONSTANT

Server <- const_1518107340940127000

\* CONSTANT declarations

CONSTANT Candidate = Candidate

\* SYMMETRY definition

SYMMETRY symm_1518107340940128000

\* CONSTRAINT definition

CONSTRAINT

constr_1518107340940129000

\* SPECIFICATION definition

SPECIFICATION

spec_1518107340940130000

\* INVARIANT definition

INVARIANT

inv_1518107340940131000

general/performance/MongoRepl/MC.tla

0 → 100644
+42 −0
Original line number Diff line number Diff line 
---- MODULE MC ----

EXTENDS RaftMongo, TLC



\* MV CONSTANT declarations@modelParameterConstants

CONSTANTS

v1

----



\* MV CONSTANT declarations@modelParameterConstants

CONSTANTS

s1, s2, s3

----



\* MV CONSTANT definitions Value

const_1518107340940126000 == 

{v1}

----



\* MV CONSTANT definitions Server

const_1518107340940127000 == 

{s1, s2, s3}

----



\* SYMMETRY definition

symm_1518107340940128000 == 

Permutations(const_1518107340940127000)

----



\* CONSTRAINT definition @modelParameterContraint:0

constr_1518107340940129000 ==

/\ \forall i \in Server: globalCurrentTerm <= 6

/\ \forall i \in Server: Len(log[i]) <= 15

----

\* SPECIFICATION definition @modelBehaviorSpec:0

spec_1518107340940130000 ==

Spec

----

\* INVARIANT definition @modelCorrectnessInvariants:0

inv_1518107340940131000 ==

NeverRollbackCommitted

----

=============================================================================

general/performance/MongoRepl/README.md

0 → 100644
+38 −0
Original line number Diff line number Diff line 
# This is a snapshot of the repository at https://github.com/visualzhou/mongo-repl-tla from which we copied the spec for TLC performance testing! We claim no authorship of this specification.

---------------------------





This is an attempt to model a simplified part of the replication system of MongoDB in TLA+.



## Spec

MongoDB secondaries pull oplogs from any nodes that have more up-to-date oplogs, which is different than the push model in Raft. This spec models the gossip protocol with two synchronized actions: AppendOplog and RollbackOplog.



The spec also simplifies the election protocol. Every election will succeed in one shot, including sending and replying vote requests and learning the new term.



## Model Checking

I have successfully run model checker on the spec with a small model that has:

- 3 nodes (symmetrical model value)

- Term up to 3

- # of logs up to 10



State constraint:

```

/\ \forall i \in Server: globalCurrentTerm <= 3

/\ \forall i \in Server: Len(log[i]) <= 10

```

Invarients to check:

- NeverRollbackCommitted



The model checker generates 7778 distinct states and passes.



## Play with the Spec

To play with the spec, you may comment out Line 112 in RollbackCommitted action, which specifies that an oplog entry replicated to the majority nodes only **in the current term** can be considered as "committed". Otherwise, secondaries syncing from the the old primary will report the commit level to the old primary even though they have voted for the new primary. This differs from the Raft protocol. In Raft, voting for a new primary implies not accepting any logs from old leaders.



Commenting out Line 112 will cause the model checker to fail, giving a simple concrete failure case.



1. Node 1 becomes the primary in term 2 and writes [index: 1, term: 2] to its oplog.

2. Node 3 wins an election in term 3 without the oplog on Node 1 and writes [index: 1, term: 3].

3. Node 2 replicates [index: 1, term: 2] from Node 1, making this oplog entry replicated on the majority nodes, but it will be rolled back after syncing from Node 3.



## Conclusion

We have found the exact same issue in MongoDB code. [SERVER-22136](https://jira.mongodb.org/browse/SERVER-22136) tracks the fix to notify the old primary of the new term. We've never encountered this issue in testing or in the field and only found it by reasoning about the edge cases. This shows writing and model checking TLA+ specs is an excellent alternative way to find and verify edge cases.

general/performance/MongoRepl/RaftMongo.tla

0 → 100644
+154 −0
Original line number Diff line number Diff line 
--------------------------------- MODULE RaftMongo ---------------------------------

\* This is the formal specification for the Raft consensus algorithm in MongoDB



EXTENDS Naturals, FiniteSets, Sequences, TLC



\* The set of server IDs

CONSTANTS Server



\* The set of requests that can go into the log

CONSTANTS Value



\* Server states.

\* Candidate is not used, but this is fine.

CONSTANTS Follower, Candidate, Leader



\* A reserved value.

CONSTANTS Nil



----

\* Global variables



\* The server's term number.

VARIABLE globalCurrentTerm



----

\* The following variables are all per server (functions with domain Server).



\* The server's state (Follower, Candidate, or Leader).

VARIABLE state

serverVars == <<globalCurrentTerm, state>>



\* A Sequence of log entries. The index into this sequence is the index of the

\* log entry. Unfortunately, the Sequence module defines Head(s) as the entry

\* with index 1, so be careful not to use that!

VARIABLE log

logVars == <<log>>



\* End of per server variables.

----



\* All variables; used for stuttering (asserting state hasn't changed).

vars == <<serverVars, logVars>>



----

\* Helpers



\* The set of all quorums. This just calculates simple majorities, but the only

\* important property is that every quorum overlaps with every other.

Quorum == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)}



\* The term of the last entry in a log, or 0 if the log is empty.

LogTerm(i, index) == IF index = 0 THEN 0 ELSE log[i][index].term

LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term



\* Return the minimum value from a set, or undefined if the set is empty.

Min(s) == CHOOSE x \in s : \A y \in s : x <= y

\* Return the maximum value from a set, or undefined if the set is empty.

Max(s) == CHOOSE x \in s : \A y \in s : x >= y



----

\* Define initial values for all variables



InitServerVars == /\ globalCurrentTerm = 1

                  /\ state             = [i \in Server |-> Follower]

InitLogVars == /\ log          = [i \in Server |-> << >>]

Init == /\ InitServerVars

        /\ InitLogVars



----

\* Message handlers

\* i = recipient, j = sender, m = message



AppendOplog(i, j) ==

    /\ Len(log[i]) < Len(log[j])

    /\ LastTerm(log[i]) = LogTerm(j, Len(log[i]))

    /\ log' = [log EXCEPT ![i] = Append(log[i], log[j][Len(log[i]) + 1])]

    /\ UNCHANGED <<serverVars>>



CanRollbackOplog(i, j) ==

    /\ Len(log[i]) > 0

    /\ \* The log with later term is more up-to-date

       LastTerm(log[i]) < LastTerm(log[j])

    /\

       \/ Len(log[i]) > Len(log[j])

       \* There seems no short-cut of OR clauses, so I have to specify the negative case

       \/ /\ Len(log[i]) <= Len(log[j])

          /\ LastTerm(log[i]) /= LogTerm(j, Len(log[i]))



RollbackOplog(i, j) ==

    /\ CanRollbackOplog(i, j)

    \* Rollback 1 oplog entry

    /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> log[i][index2]]

         IN log' = [log EXCEPT ![i] = new]

    /\ UNCHANGED <<serverVars>>





\* RollbackCommitted and NeverRollbackCommitted are not actions.

\* They are used for verification.

RollbackCommitted(i) ==

    LET

        \* The set of nodes that has log[me][logIndex] in their oplog

        Agree(me, logIndex) ==

            { node \in Server :

                /\ Len(log[node]) >= logIndex

                /\ LogTerm(me, logIndex) = LogTerm(node, logIndex) }

        IsCommitted(me, logIndex) ==

            /\ Agree(me, logIndex) \in Quorum

            \* If we comment out the following line, a replicated log entry from old primary will voilate the safety.

            \* [ P (2), S (), S ()]

            \* [ S (2), S (), P (3)]

            \* [ S (2), S (2), P (3)] !!! the log from term 2 shouldn't be considered as committed.

            /\ LogTerm(me, logIndex) = globalCurrentTerm

    IN  \E j \in Server:

        /\ CanRollbackOplog(i, j)

        /\ IsCommitted(i, Len(log[i]))



NeverRollbackCommitted ==

    \A i \in Server: ~RollbackCommitted(i)



\* i = the new primary node.

BecomePrimaryByMagic(i) ==

    LET notBehind(me, j) ==

            \/ LastTerm(log[me]) > LastTerm(log[j])

            \/ /\ LastTerm(log[me]) = LastTerm(log[j])

               /\ Len(log[me]) >= Len(log[j])

        ayeVoters(me) ==

            { index \in Server : notBehind(me, index) }

    IN /\ ayeVoters(i) \in Quorum

       /\ state' = [index \in Server |-> IF index = i THEN Leader ELSE Follower]

       /\ globalCurrentTerm' = globalCurrentTerm + 1

       /\ UNCHANGED <<logVars>>



\* Leader i receives a client request to add v to the log.

ClientWrite(i, v) ==

    /\ state[i] = Leader

    /\ LET entry == [term  |-> globalCurrentTerm,

                     value |-> v]

           newLog == Append(log[i], entry)

       IN  log' = [log EXCEPT ![i] = newLog]

    /\ UNCHANGED <<serverVars>>



----

\* Defines how the variables may transition.

Next == /\

           \/ \E i,j \in Server : AppendOplog(i, j)

           \/ \E i,j \in Server : RollbackOplog(i, j)

           \/ \E i \in Server : BecomePrimaryByMagic(i)

           \/ \E i \in Server, v \in Value : ClientWrite(i, v)



\* The specification must start with the initial state and transition according

\* to Next.

Spec == Init /\ [][Next]_vars



===============================================================================

general/performance/SwarmKit/EventCounter.tla

0 → 100644
+25 −0
Original line number Diff line number Diff line 
---------------------------- MODULE EventCounter ----------------------------



EXTENDS Integers



\* The number of ``events'' that have occurred (always 0 if we're not keeping track).

VARIABLE nEvents



\* The maximum number of events to allow, or ``-1'' for unlimited.

maxEvents == -1



InitEvents ==

  nEvents = 0       \* Start with the counter at zero



(* If we're counting events, increment the event counter.

   We don't increment the counter when we don't have a maximum because that

   would make the model infinite.

   Actions tagged with CountEvent cannot happen once nEvents = maxEvents. *)

CountEvent ==

  IF maxEvents = -1 THEN

    UNCHANGED nEvents

  ELSE

    /\ nEvents < maxEvents

    /\ nEvents' = nEvents + 1



=============================================================================
 
 No newline at end of file

general/performance/SwarmKit/MC.cfg

0 → 100644
+15 −0
Original line number Diff line number Diff line 
SPECIFICATION Spec



CONSTANT TaskId = {t1, t2}

CONSTANT ServiceId = {s1, s1}

CONSTANT Node = {n1, n2}

CONSTANT maxTerminated = 1

CONSTANT maxReplicas = 1

CONSTANT unassigned = unassigned

CONSTANT global = global



INVARIANT TypeOK

INVARIANT Inv



PROPERTY TransitionsOK

PROPERTY EventuallyAsDesired

general/performance/SwarmKit/MC.tla

0 → 100644
+4 −0
Original line number Diff line number Diff line 
----------- MODULE MC -----------

EXTENDS SwarmKit



=================================

general/performance/SwarmKit/README.md

0 → 100644
+1 −0
Original line number Diff line number Diff line 
# This is a snapshot of the tlaplus folder of the repository at https://github.com/talex5/swarmkit/tree/c43c5852be355dae2e32328c17b8885cfc86600f/design/tla/ - released under the Apache 2 license - from which we copied the spec for TLC performance testing! We claim no authorship of this specification.

general/performance/SwarmKit/Tasks.tla

0 → 100644
+112 −0
Original line number Diff line number Diff line 
---------------------------- MODULE Tasks ----------------------------------



EXTENDS TLC, Types



VARIABLE tasks          \* The set of currently-allocated tasks



(* The expected type of each variable. TLA+ is an untyped language, but the model checker

   can check that TasksTypeOK is true for every reachable state. *)

TasksTypeOK ==

  \* `tasks' is a subset of the set of all possible tasks

  /\ tasks \in SUBSET Task



(* Update `tasks' by performing each update in `f', which is a function

   mapping old tasks to new ones. *)

UpdateTasks(f) ==

  /\ Assert(\A t \in DOMAIN f : t \in tasks, "An old task does not exist!")

  /\ Assert(\A t \in DOMAIN f :

                LET t2 == f[t]

                IN                        \* The updated version of `t' must have

                /\ t.id      = t2.id      \* the same task ID,

                /\ t.service = t2.service \* the same service ID,

                /\ VSlot(t)  = VSlot(t2), \* and the same vslot.

            "An update changes a task's identity!")

  \* Remove all the old tasks and add the new ones:

  /\ tasks' = (tasks \ DOMAIN f) \union Range(f)



(* A `new' task belonging to service `sid' with the given slot, id, and desired state. *)

NewTask(sid, vslot, id, desired_state) ==

  [

    id            |-> id,

    service       |-> sid,

    status        |-> [ state |-> new ],

    desired_state |-> desired_state,

    node          |-> IF vslot \in Node THEN vslot ELSE unassigned,

    slot          |-> IF vslot \in Slot THEN vslot ELSE global

  ]





\* A special ``state'' used when a task doesn't exist.

null == "null"



(* All the possible transitions, grouped by the component that performs them. *)

Transitions == [

  orchestrator |-> {

    << null, new >>

  },



  allocator |-> {

    << new, pending >>

  },



  scheduler |-> {

    << pending, assigned >>

  },



  agent |-> {

    << assigned, accepted >>,

    << accepted, preparing >>,

    << preparing, ready >>,

    << ready, starting >>,

    << starting, running >>,



    << assigned, rejected >>,

    << accepted, rejected >>,

    << preparing, rejected >>,

    << ready, rejected >>,

    << starting, rejected >>,



    << running, complete >>,

    << running, failed >>,



    << running, shutdown >>,



    << assigned, orphaned >>,

    << accepted, orphaned >>,

    << preparing, orphaned >>,

    << ready, orphaned >>,

    << starting, orphaned >>,

    << running, orphaned >>

  },



  reaper |-> {

    << new, null >>,

    << pending, null >>,

    << rejected, null >>,

    << complete, null >>,

    << failed, null >>,

    << shutdown, null >>,

    << orphaned, null >>

  }

]



(* Check that `Transitions' itself is OK. *)

TransitionTableOK ==

  \* No transition moves to a lower-ranked state:

  /\ \A actor \in DOMAIN Transitions :

     \A trans \in Transitions[actor] :

        \/ trans[1] = null

        \/ trans[2] = null

        \/ trans[1] \preceq trans[2]

  (* Every source state has exactly one component which handles transitions out of that state.

     Except for the case of the reaper removing `new' and `pending' tasks that are flagged

     for removal. *)

  /\ \A a1, a2 \in DOMAIN Transitions :

     LET exceptions == { << new, null >>, << pending, null >> }

          Source(a) == { s[1] : s \in Transitions[a] \ exceptions}

     IN  a1 # a2 =>

           Source(a1) \intersect Source(a2) = {}



ASSUME TransitionTableOK  \* Note: ASSUME means ``check'' to TLC



=============================================================================
 
 No newline at end of file

general/performance/SwarmKit/Types.tla

0 → 100644
+124 −0
Original line number Diff line number Diff line 
------------------------------- MODULE Types -------------------------------



EXTENDS Naturals, FiniteSets



(* A generic operator to get the range of a function (the set of values in a map): *)

Range(S) == { S[i] : i \in DOMAIN S }



(* The set of worker nodes.



   Note: a CONSTANT is an input to the model. The model should work with any set of nodes you provide.



   TODO: should cope with this changing at runtime, and with draining nodes. *)

CONSTANT Node



(* A special value indicating that a task is not yet assigned to a node.



   Note: this TLA+ CHOOSE idiom just says to pick some value that isn't a Node (e.g. `null'). *)

unassigned == CHOOSE n : n \notin Node



(* The type (set) of service IDs (e.g. `Int' or `String').

   When model checking, this will be some small set (e.g. {"s1", "s2"}). *)

CONSTANT ServiceId



(* The type of task IDs. *)

CONSTANT TaskId



(* The maximum possible value for `replicas' in ServiceSpec. *)

CONSTANT maxReplicas

ASSUME maxReplicas \in Nat

Slot == 1..maxReplicas  \* Possible slot numbers



(* A special value (e.g. `-1') indicating that we want one replica running on each node: *)

global == CHOOSE x : x \notin Nat



(* The type of a description of a service (a struct/record).

   This is provided by, and only changed by, the user. *)

ServiceSpec == [

  (* The replicas field is either a count giving the desired number of replicas,

     or the special value `global'. *)

  replicas : 0..maxReplicas \union {global},

  remove   : BOOLEAN    \* The user wants to remove this service

]



(* The possible states for a task: *)

new == "new"

pending == "pending"

assigned == "assigned"

accepted == "accepted"

preparing == "preparing"

ready == "ready"

starting == "starting"

running == "running"

complete == "complete"

shutdown == "shutdown"

failed == "failed"

rejected == "rejected"

remove == "remove"      \* Only used as a ``desired state'', not an actual state

orphaned == "orphaned"



(* Every state has a rank. It is only possible for a task to change

   state to a state with a higher rank (later in this sequence). *)

order == << new, pending, assigned, accepted,

             preparing, ready, starting,

             running,

             complete, shutdown, failed, rejected,

             remove, orphaned >>



(* Maps a state to its position in `order' (e.g. StateRank(new) = 1): *)

StateRank(s) == CHOOSE i \in DOMAIN order : order[i] = s



(* Convenient notation for comparing states: *)

s1 \prec s2   == StateRank(s1) < StateRank(s2)

s1 \preceq s2 == StateRank(s1) <= StateRank(s2)



(* The set of possible states ({new, pending, ...}): *)

TaskState == Range(order) \ {remove}



(* Possibly this doesn't need to be a record, but we might want to add extra fields later. *)

TaskStatus == [

  state : TaskState

]



(* The state that SwarmKit wants to the task to be in. *)

DesiredState == { ready, running, shutdown, remove }



(* This has every field mentioned in `task_model.md' except for `spec', which

   it doesn't seem to use for anything.



   `desired_state' can be any state, although currently we only ever set it to one of

    {ready, running, shutdown, remove}. *)

Task == [

  id : TaskId,                      \* To uniquely identify this task

  service : ServiceId,              \* The service that owns the task

  status : TaskStatus,              \* The current state

  desired_state : DesiredState,     \* The state requested by the orchestrator

  node : Node \union {unassigned},  \* The node on which the task should be run

  slot : Slot \union {global}       \* A way of tracking related tasks

]



(* The current state of task `t'. *)

State(t) == t.status.state



(* A task is runnable if it is running or could become running in the future. *)

Runnable(t) == State(t) \preceq running



(* A task's ``virtual slot'' is its actual slot for replicated services,

   but its node for global ones. *)

VSlot(t) ==

  IF t.slot = global THEN t.node ELSE t.slot



(* In the real SwarmKit, a task's ID is just its taskId field.

   However, this requires lots of IDs, which is expensive for model checking.

   So instead, we will identify tasks by their << serviceId, vSlot, taskId >>

   triple, and only require taskId to be unique within its vslot. *)

ModelTaskId == ServiceId \X (Slot \union Node) \X TaskId



(* A unique identifier for a task, which never changes. *)

Id(t) ==

  << t.service, VSlot(t), t.id >>   \* A ModelTaskId



(* The ModelTaskIds of a set of tasks. *)

IdSet(S) == { Id(t) : t \in S }



=============================================================================

general/performance/SwarmKit/WorkerImpl.tla

0 → 100644
+321 −0
Original line number Diff line number Diff line 
---------------------------- MODULE WorkerImpl ----------------------------------



EXTENDS TLC, Types, Tasks, EventCounter



(*

`WorkerSpec' provides a high-level specification of worker nodes that only refers to

the state of the tasks recorded in SwarmKit's store. This specification (WorkerImpl)

refines WorkerSpec by also modelling the state of the containers running on a node.

It should be easier to see that this lower-level specification corresponds to what

actually happens on worker nodes.



The reason for having this in a separate specification is that including the container

state greatly increases the number of states to be considered and so slows down model

checking. Instead of checking



  SwarmKit /\ WorkerImpl => EventuallyAsDesired



(which is very slow), we check two separate expressions:



  SwarmKit /\ WorkerSpec => EventuallyAsDesired

  WorkerImpl => WorkerSpec



TLAPS can check that separating the specification in this way makes sense: *)

THEOREM ASSUME TEMPORAL SwarmKit, TEMPORAL WorkerSpec,

               TEMPORAL WorkerImpl, TEMPORAL EventuallyAsDesired,

               TEMPORAL Env,  \* A simplified version of SwarmKit

               SwarmKit /\ WorkerSpec => EventuallyAsDesired,

               Env /\ WorkerImpl => WorkerSpec,

               SwarmKit => Env

        PROVE  SwarmKit /\ WorkerImpl => EventuallyAsDesired

OBVIOUS



\* This worker's node ID

CONSTANT node

ASSUME node \in Node



VARIABLES nodes         \* Defined in WorkerSpec.tla

VARIABLE containers     \* The actual container state on the node, indexed by ModelTaskId



(* The high-level specification of worker nodes.

   This module should be a refinement of `WS'. *)

WS == INSTANCE WorkerSpec



terminating == "terminating"        \* A container which we're trying to stop



(* The state of an actual container on a worker node. *)

ContainerState == { running, terminating, complete, failed }



(* A running container finishes running on its own (or crashes). *)

ContainerExit ==

  /\ UNCHANGED << nodes, tasks >>

  /\ CountEvent

  /\ \E id \in DOMAIN containers,

        s2 \in {failed, complete} :      \* Either a successful or failed exit status

        /\ containers[id] = running

        /\ containers' = [containers EXCEPT ![id] = s2]



(* A running container finishes because we stopped it. *)

ShutdownComplete ==

  /\ UNCHANGED << nodes, tasks, nEvents >>

  /\ \E id \in DOMAIN containers :

        /\ containers[id] = terminating

        /\ containers' = [containers EXCEPT ![id] = failed]



(* SwarmKit thinks the node is up. i.e. the agent is connected to a manager. *)

IsUp(n) == WS!IsUp(n)



(* The new value that `containers' should take after getting an update from the

   managers. If the managers asked us to run a container and then stop mentioning

   that task, we shut the container down and (once stopped) remove it. *)

DesiredContainers ==

  LET WantShutdown(id) ==

        \* The managers stop mentioning the task, or ask for it to be stopped.

        \/ id \notin IdSet(tasks)

        \/ running \prec (CHOOSE t \in tasks : Id(t) = id).desired_state

      (* Remove containers that no longer have tasks, once they've stopped. *)

      rm == { id \in DOMAIN containers :

                  /\ containers[id] \in { complete, failed }

                  /\ id \notin IdSet(tasks) }

  IN [ id \in DOMAIN containers \ rm |->

           IF containers[id] = running /\ WantShutdown(id) THEN terminating

           ELSE containers[id]

     ]



(* The updates that SwarmKit should apply to its store to bring it up-to-date

   with the real state of the containers. *)

RequiredTaskUpdates ==

  LET \* Tasks the manager is expecting news about:

      oldTasks == { t \in tasks : t.node = node /\ State(t) = running }

      \* The state to report for task `t':

      ReportFor(t) ==

        IF Id(t) \notin DOMAIN containers THEN \* We were asked to forget about this container.

          shutdown \* SwarmKit doesn't care which terminal state we finish in.

        ELSE IF /\ containers[Id(t)] = failed       \* It's terminated and

                /\ t.desired_state = shutdown THEN  \* we wanted to shut it down,

          shutdown \* Report a successful shutdown

        ELSE IF containers[Id(t)] = terminating THEN

          running  \* SwarmKit doesn't record progress of the shutdown

        ELSE

          containers[Id(t)]  \* Report the actual state

  IN [ t \in oldTasks |-> [ t EXCEPT !.status.state = ReportFor(t) ]]



(* Our node synchronises its state with a manager. *)

DoSync ==

   /\ containers' = DesiredContainers

   /\ UpdateTasks(RequiredTaskUpdates)



(* Try to advance containers towards `desired_state' if we're not there yet.



   XXX: do we need a connection to the manager to do this, or can we make progress

   while disconnected and just report the final state?

*)

ProgressTask ==

  /\ UNCHANGED << nodes, nEvents >>

  /\ \E t  \in tasks,

        s2 \in TaskState :   \* The state we want to move to

        LET t2 == [t EXCEPT !.status.state = s2]

        IN

        /\ s2 \preceq t.desired_state       \* Can't be after the desired state

        /\ << State(t), State(t2) >> \in {  \* Possible ``progress'' (desirable) transitions

             << assigned, accepted >>,

             << accepted, preparing >>,

             << preparing, ready >>,

             << ready, starting >>,

             << starting, running >>

           }

        /\ IsUp(t.node)                     \* Node must be connected to SwarmKit

        /\ IF s2 = running THEN

              \* The container started running

              containers' = Id(t) :> running @@ containers

           ELSE

              UNCHANGED containers

        /\ UpdateTasks(t :> t2)



(* The agent on the node synchronises with a manager. *)

SyncWithManager ==

  /\ UNCHANGED << nodes, nEvents >>

  /\ IsUp(node)

  /\ DoSync



(* We can reject a task once we're responsible for it (it has reached `assigned')

   until it reaches the `running' state.

   Note that an ``accepted'' task can still be rejected. *)

RejectTask ==

  /\ UNCHANGED << nodes, containers >>

  /\ CountEvent

  /\ \E t \in tasks :

       /\ State(t) \in { assigned, accepted, preparing, ready, starting }

       /\ t.node = node

       /\ IsUp(node)

       /\ UpdateTasks(t :> [t EXCEPT !.status.state = rejected])



(* The dispatcher notices that the worker is down (the connection is lost). *)

WorkerDown ==

  /\ UNCHANGED << tasks, containers >>

  /\ CountEvent

  /\ \E n \in Node :

       /\ IsUp(n)

       /\ nodes' = [nodes EXCEPT ![n] = WS!nodeDown]



(* When the node reconnects to the cluster, it gets an assignment set from the dispatcher

   which does not include any tasks that have been marked orphaned and then deleted.

   Any time an agent gets an assignment set that does not include some task it has running,

   it shuts down those tasks.



   We model this separately with the `SyncWithManager' action. *)

WorkerUp ==

  /\ UNCHANGED << nEvents, containers, tasks >>

  /\ \E n \in Node :

       /\ ~IsUp(n)

       /\ nodes' = [nodes EXCEPT ![n] = WS!nodeUp]



(* Tasks assigned to a node and for which the node is responsible. *)

TasksOwnedByNode(n) == { t \in tasks :

  /\ t.node = n

  /\ assigned \preceq State(t)

  /\ State(t) \prec remove

}



(* If SwarmKit sees a node as down for a long time (48 hours or so) then

   it marks all the node's tasks as orphaned.

   Note that this sets the actual state, not the desired state.



   ``Moving a task to the Orphaned state is not desirable,

   because it's the one case where we break the otherwise invariant

   that the agent sets all states past ASSIGNED.''

*)

OrphanTasks ==

  /\ UNCHANGED << nodes, containers, nEvents >>

  /\ LET affected == { t \in TasksOwnedByNode(node) : Runnable(t) }

     IN

     /\ ~IsUp(node)    \* Our connection to the agent is down

     /\ UpdateTasks([ t \in affected |->

                         [t EXCEPT !.status.state = orphaned] ])



(* The worker reboots. All containers are terminated. *)

WorkerReboot ==

  /\ UNCHANGED << nodes, tasks >>

  /\ CountEvent

  /\ containers' = [ id \in DOMAIN containers |->

                       LET state == containers[id]

                       IN  CASE state \in {running, terminating} -> failed

                             [] state \in {complete, failed}     -> state

                   ]



(* Actions we require to happen eventually when possible. *)

AgentProgress ==

  \/ ProgressTask

  \/ OrphanTasks

  \/ WorkerUp

  \/ ShutdownComplete

  \/ SyncWithManager



(* All actions of the agent/worker. *)

Agent ==

  \/ AgentProgress

  \/ RejectTask

  \/ WorkerDown

  \/ ContainerExit

  \/ WorkerReboot



-------------------------------------------------------------------------------

\* A simplified model of the rest of the system



(* A new task is created. *)

CreateTask ==

  /\ UNCHANGED << containers, nEvents, nodes >>

  /\ \E t \in Task :    \* `t' is the new task

      \* Don't reuse IDs (only really an issue for model checking)

      /\ Id(t) \notin IdSet(tasks)

      /\ Id(t) \notin DOMAIN containers

      /\ State(t) = new

      /\ t.desired_state \in { ready, running }

      /\ \/ /\ t.node = unassigned  \* A task for a replicated service

            /\ t.slot \in Slot

         \/ /\ t.node \in Node      \* A task for a global service

            /\ t.slot = global

      /\ ~\E t2 \in tasks : \* All tasks of a service have the same mode

            /\ t.service = t2.service

            /\ (t.slot = global) # (t2.slot = global)

      /\ tasks' = tasks \union {t}



(* States before `assigned' aren't shared with worker nodes, so modelling them

   isn't very useful. You can use this in a model to override `CreateTask' to

   speed things up a bit. It creates tasks directly in the `assigned' state. *)

CreateTaskQuick ==

  /\ UNCHANGED << containers, nEvents, nodes >>

  /\ \E t \in Task :

      /\ Id(t) \notin IdSet(tasks)

      /\ Id(t) \notin DOMAIN containers

      /\ State(t) = assigned

      /\ t.desired_state \in { ready, running }

      /\ t.node \in Node

      /\ t.slot \in Slot \union {global}

      /\ ~\E t2 \in tasks : \* All tasks of a service have the same mode

            /\ t.service = t2.service

            /\ (t.slot = global) # (t2.slot = global)

      /\ tasks' = tasks \union {t}



(* The state or desired_state of a task is updated. *)

UpdateTask ==

  /\ UNCHANGED << containers, nEvents, nodes >>

  /\ \E t \in tasks, t2 \in Task :  \* `t' becomes `t2'

        /\ Id(t) = Id(t2)           \* The ID can't change

        /\ State(t) # State(t2) =>  \* If the state changes then

             \E actor \in DOMAIN Transitions :  \* it is a legal transition

                 /\ actor = "agent"  =>  t.node # node    \* and not one our worker does

                 /\ << State(t), State(t2) >> \in Transitions[actor]

        \* When tasks reach the `assigned' state, they must have a node

        /\ IF State(t2) = assigned /\ t.node = unassigned THEN t2.node \in Node

                                                          ELSE t2.node = t.node

        /\ UpdateTasks(t :> t2)



(* The reaper removes a task. *)

RemoveTask ==

  /\ UNCHANGED << containers, nEvents, nodes >>

  /\ \E t \in tasks :

      /\ << State(t), null >> \in Transitions.reaper

      /\ tasks' = tasks \ {t}



(* Actions of our worker's environment (i.e. SwarmKit and other workers). *)

OtherComponent ==

  \/ CreateTask

  \/ UpdateTask

  \/ RemoveTask



-------------------------------------------------------------------------------

\* A complete system



vars == << tasks, nEvents, nodes, containers >>



Init ==

  /\ tasks = {}

  /\ containers = << >>

  /\ nodes = [ n \in Node |-> WS!nodeUp ]

  /\ InitEvents



Next ==

  \/ OtherComponent

  \/ Agent



(* The specification for our worker node. *)

Impl == Init /\ [][Next]_vars /\ WF_vars(AgentProgress)



-------------------------------------------------------------------------------



TypeOK ==

  /\ TasksTypeOK

  \* The node's container map maps IDs to states

  /\ DOMAIN containers \in SUBSET ModelTaskId

  /\ containers \in [ DOMAIN containers -> ContainerState ]



wsVars == << tasks, nEvents, nodes >>



(* We want to check that a worker implementing `Impl' is also implementing

   `WorkerSpec'. i.e. we need to check that Impl => WSSpec. *)

WSSpec ==

  /\ [][WS!Agent \/ OtherComponent]_wsVars

  /\ WF_wsVars(WS!AgentProgress)



=============================================================================

general/performance/SwarmKit/WorkerSpec.tla

0 → 100644
+133 −0
Original line number Diff line number Diff line 
----------------------------- MODULE WorkerSpec -----------------------------



EXTENDS Types, Tasks, EventCounter



VARIABLE nodes          \* Maps nodes to SwarmKit's view of their NodeState



(* The possible states of a node, as recorded by SwarmKit. *)

nodeUp   == "up"

nodeDown == "down"

NodeState == { nodeUp, nodeDown }



WorkerTypeOK ==

  \* Nodes are up or down

  /\ nodes \in [ Node -> NodeState ]



-----------------------------------------------------------------------------



\*  Actions performed by worker nodes (actually, by the dispatcher on their behalf)



(* SwarmKit thinks the node is up. i.e. the agent is connected to a manager. *)

IsUp(n) == nodes[n] = nodeUp



(* Try to advance containers towards `desired_state' if we're not there yet. *)

ProgressTask ==

  /\ UNCHANGED << nodes, nEvents >>

  /\ \E t  \in tasks,

        s2 \in TaskState :   \* The state we want to move to

        LET t2 == [t EXCEPT !.status.state = s2]

        IN

        /\ s2 \preceq t.desired_state       \* Can't be after the desired state

        /\ << State(t), State(t2) >> \in {  \* Possible ``progress'' (desirable) transitions

             << assigned, accepted >>,

             << accepted, preparing >>,

             << preparing, ready >>,

             << ready, starting >>,

             << starting, running >>

           }

        /\ IsUp(t.node)                     \* Node must be connected to SwarmKit

        /\ UpdateTasks(t :> t2)



(* A running container finishes because we stopped it. *)

ShutdownComplete ==

  /\ UNCHANGED << nodes, nEvents >>

  /\ \E t \in tasks :

     /\ t.desired_state \in {shutdown, remove}                  \* We are trying to stop it

     /\ State(t) = running                                      \* It is currently running

     /\ IsUp(t.node)

     /\ UpdateTasks(t :> [t EXCEPT !.status.state = shutdown])  \* It becomes shutdown



(* A node can reject a task once it's responsible for it (it has reached `assigned')

   until it reaches the `running' state.

   Note that an ``accepted'' task can still be rejected. *)

RejectTask ==

  /\ UNCHANGED << nodes >>

  /\ CountEvent

  /\ \E t \in tasks :

       /\ State(t) \in { assigned, accepted, preparing, ready, starting }

       /\ IsUp(t.node)

       /\ UpdateTasks(t :> [t EXCEPT !.status.state = rejected])



(* We notify the managers that some running containers have finished.

   There might be several updates at once (e.g. if we're reconnecting). *)

ContainerExit ==

  /\ UNCHANGED << nodes >>

  /\ CountEvent

  /\ \E n \in Node :

        /\ IsUp(n)

        /\ \E ts \in SUBSET { t \in tasks : t.node = n /\ State(t) = running } :

           \* Each container could have ended in either state:

           \E s2 \in [ ts -> { failed, complete } ] :

             UpdateTasks( [ t \in ts |->

                             [t EXCEPT !.status.state =

                               \* Report `failed' as `shutdown' if we wanted to shut down

                               IF s2[t] = failed /\ t.desired_state = shutdown THEN shutdown

                               ELSE s2[t]]

                        ] )



(* Tasks assigned to a node and for which the node is responsible. *)

TasksOwnedByNode(n) == { t \in tasks :

  /\ t.node = n

  /\ assigned \preceq State(t)

  /\ State(t) \prec remove

}



(* The dispatcher notices that the worker is down (the connection is lost). *)

WorkerDown ==

  /\ UNCHANGED << tasks >>

  /\ CountEvent

  /\ \E n \in Node :

       /\ IsUp(n)

       /\ nodes' = [nodes EXCEPT ![n] = nodeDown]



(* When the node reconnects to the cluster, it gets an assignment set from the dispatcher

   which does not include any tasks that have been marked orphaned and then deleted.

   Any time an agent gets an assignment set that does not include some task it has running,

   it shuts down those tasks. *)

WorkerUp ==

  /\ UNCHANGED << tasks, nEvents >>

  /\ \E n \in Node :

       /\ ~IsUp(n)

       /\ nodes' = [nodes EXCEPT ![n] = nodeUp]



(* If SwarmKit sees a node as down for a long time (48 hours or so) then

   it marks all the node's tasks as orphaned.



   ``Moving a task to the Orphaned state is not desirable,

   because it's the one case where we break the otherwise invariant

   that the agent sets all states past ASSIGNED.''

*)

OrphanTasks ==

  /\ UNCHANGED << nodes, nEvents >>

  /\ \E n \in Node :

       LET affected == { t \in TasksOwnedByNode(n) : Runnable(t) }

       IN

       /\ ~IsUp(n)    \* Node `n' is still detected as down

       /\ UpdateTasks([ t \in affected |->

                         [t EXCEPT !.status.state = orphaned] ])



(* Actions we require to happen eventually when possible. *)

AgentProgress ==

  \/ ProgressTask

  \/ ShutdownComplete

  \/ OrphanTasks

  \/ WorkerUp



(* All actions of the agent/worker. *)

Agent ==

  \/ AgentProgress

  \/ RejectTask

  \/ ContainerExit

  \/ WorkerDown



=============================================================================

org.lamport.tla.toolbox.editor.basic/.classpath

+1 −1
Original line number Diff line number Diff line 
<?xml version="1.0" encoding="UTF-8"?>

<classpath>

	<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.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>

	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>

	<classpathentry kind="src" path="src"/>

	<classpathentry kind="output" path="bin"/>

org.lamport.tla.toolbox.editor.basic/.settings/org.eclipse.jdt.core.prefs

+3 −4
Original line number Diff line number Diff line 
#Mon May 09 12:19:15 CEST 2011

eclipse.preferences.version=1

org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled

org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5

org.eclipse.jdt.core.compiler.compliance=1.5

org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8

org.eclipse.jdt.core.compiler.compliance=1.8

org.eclipse.jdt.core.compiler.problem.assertIdentifier=error

org.eclipse.jdt.core.compiler.problem.enumIdentifier=error

org.eclipse.jdt.core.compiler.source=1.5
 
org.eclipse.jdt.core.compiler.source=1.8

org.lamport.tla.toolbox.editor.basic/META-INF/MANIFEST.MF

+9 −4
Original line number Diff line number Diff line
@@ -14,10 +14,15 @@ Require-Bundle: org.eclipse.ui, 
 org.eclipse.core.resources,

 org.eclipse.ui.workbench.texteditor,

 org.eclipse.ui.views,

 org.eclipse.ui.forms

Bundle-RequiredExecutionEnvironment: J2SE-1.5

 org.eclipse.ui.forms,

 org.eclipse.core.filesystem

Bundle-RequiredExecutionEnvironment: JavaSE-1.8

Bundle-ActivationPolicy: lazy

Import-Package: org.eclipse.e4.core.services.events,

 org.eclipse.ui.forms

Import-Package: org.eclipse.e4.core.di.annotations;version="1.6.0",

 org.eclipse.e4.core.services.events,

 org.eclipse.ui.forms,

 org.osgi.service.event;version="1.3.1"

Export-Package: org.lamport.tla.toolbox.editor.basic,

 org.lamport.tla.toolbox.editor.basic.handlers;x-friends:="org.lamport.tla.toolbox",

 org.lamport.tla.toolbox.editor.basic.tla,

 org.lamport.tla.toolbox.editor.basic.util

org.lamport.tla.toolbox.editor.basic/plugin.xml

+26 −0
Original line number Diff line number Diff line
@@ -307,6 +307,24 @@ 
            id="org.lamport.tla.toolbox.editor.basic.DecomposeProof"

            name="Decompose Proof">

      </command>

      <command

            categoryId="org.eclipse.ui.category.textEditor"

            defaultHandler="org.lamport.tla.toolbox.util.e4.E4HandlerWrapper:org.lamport.tla.toolbox.editor.basic.handlers.PCalTranslateAutomaticallyHandler"

            description="Automatically translate PlusCal to TLA+ on TLA+ editor save."

            id="toolbox.command.module.translate.automatially"

            name="Translate PlusCal automatically">

		   <state

				class="org.eclipse.ui.handlers.RegistryToggleState:false"

				id="org.eclipse.ui.commands.toggleState">

		   </state>

      </command>

      <command

            categoryId="toolbox.command.category.module"

            defaultHandler="org.lamport.tla.toolbox.editor.basic.handlers.PCalTranslateModuleHandler"

            description="Translates PCal in the active editor"

            id="toolbox.command.module.translate.active"

            name="Translate module">

      </command>



   </extension>

   <extension
@@ -629,6 +647,14 @@ 
                    commandId="org.lamport.tla.toolbox.editor.basic.gotoMatchingParen"

                    style="push">

              </command>

              <separator

                    name="org.lamport.tla.toolbox.editor.basic.commentseparator"

                    visible="true">

              </separator>

              <command

                    commandId="toolbox.command.module.translate.automatially"

                    style="toggle">

              </command>

           </menuContribution>

         

   </extension>

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/TLAEditor.java

+31 −4
Original line number Diff line number Diff line
@@ -37,6 +37,7 @@ import org.eclipse.jface.action.Separator; 
import org.eclipse.jface.dialogs.MessageDialog;

import org.eclipse.jface.preference.IPreferenceStore;

import org.eclipse.jface.text.BadLocationException;

import org.eclipse.jface.text.FindReplaceDocumentAdapter;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IRegion;

import org.eclipse.jface.text.ITextSelection;
@@ -80,6 +81,7 @@ import org.eclipse.ui.texteditor.ITextEditorActionConstants; 
import org.eclipse.ui.texteditor.ITextEditorActionDefinitionIds;

import org.eclipse.ui.texteditor.TextOperationAction;

import org.lamport.tla.toolbox.editor.basic.actions.ToggleCommentAction;

import org.lamport.tla.toolbox.editor.basic.pcal.IPCalReservedWords;

import org.lamport.tla.toolbox.editor.basic.proof.IProofFoldCommandIds;

import org.lamport.tla.toolbox.editor.basic.proof.TLAProofFoldingStructureProvider;

import org.lamport.tla.toolbox.editor.basic.proof.TLAProofPosition;
@@ -99,7 +101,6 @@ import pcal.TLAtoPCalMapping; 
 * Basic editor for TLA+

 *

 * @author Simon Zambrovski

 * @version $Id$

 */

public class TLAEditor extends TextEditor

{
@@ -108,6 +109,11 @@ public class TLAEditor extends TextEditor 
	 * saved.

	 */

	public static final String SAVE_EVENT = "TLAEditor/save";

	/**

	 * The IEventBroker topic identifying the event sent out while the editor is

	 * being saved.

	 */

	public static final String PRE_SAVE_EVENT = "TLAEditor/presave";

	

	public static final String ID = "org.lamport.tla.toolbox.editor.basic.TLAEditor";

    private IContextService contextService = null;
@@ -445,6 +451,8 @@ public class TLAEditor extends TextEditor 
     */

    public void doSave(IProgressMonitor progressMonitor)

    {

        service.send(PRE_SAVE_EVENT, this);

        

        final IEditorInput editorInput = this.getEditorInput();

		IDocument doc = this.getDocumentProvider().getDocument(editorInput);

        String text = doc.get();
@@ -545,6 +553,7 @@ public class TLAEditor extends TextEditor 


        } // end if (historyStart > -1)

        

        super.doSave(progressMonitor);

        

		// Send out a save event through the event bus. There might be parties

		// interested in this, e.g. to regenerate the pretty printed pdf.
@@ -554,8 +563,6 @@ public class TLAEditor extends TextEditor 
        	final IFile spec = fei.getFile();

        	service.post(SAVE_EVENT, spec);

        }

        

        super.doSave(progressMonitor);

    }



    /**
@@ -742,6 +749,7 @@ public class TLAEditor extends TextEditor 
        }

    }



    @SuppressWarnings("unchecked")

	public Object getAdapter(@SuppressWarnings("rawtypes") Class required)

    {

        /* adapt to projection support */
@@ -902,6 +910,25 @@ public class TLAEditor extends TextEditor 
        return this.getSourceViewer();

    }

    

    

	public boolean hasPlusCal() {

		try {

			// Search the document for the string "--algorithm" or "--fair".

	        final IDocument doc = this.getDocumentProvider().getDocument(this.getEditorInput());

			final FindReplaceDocumentAdapter search = new FindReplaceDocumentAdapter(doc);

			IRegion find = search.find(0, IPCalReservedWords.ALGORITHM, true, true, false, false);

			if (find != null) {

				return true;

			}

			find = search.find(0, "--" + IPCalReservedWords.FAIR, true, true, false, false);

			if (find != null) {

				return true;

			}

		} catch (BadLocationException e) {

		}

		return false;

	}

    

    /**

     * Simon's comments, explaining exactly what this class is doing:

     * The class is located here, because editor does not expose the source viewer (method protected)

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/TLASourceViewerConfiguration.java

+76 −2
Original line number Diff line number Diff line 
package org.lamport.tla.toolbox.editor.basic;



import java.lang.reflect.Field;



import org.eclipse.jface.preference.IPreferenceStore;

import org.eclipse.jface.resource.JFaceResources;

import org.eclipse.jface.text.DefaultInformationControl;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IInformationControl;

import org.eclipse.jface.text.IInformationControlCreator;

import org.eclipse.jface.text.ITextHover;

import org.eclipse.jface.text.TextAttribute;

import org.eclipse.jface.text.contentassist.ContentAssistant;

import org.eclipse.jface.text.contentassist.ICompletionProposal;

import org.eclipse.jface.text.contentassist.ICompletionProposalSorter;

import org.eclipse.jface.text.contentassist.IContentAssistant;

import org.eclipse.jface.text.presentation.IPresentationReconciler;

import org.eclipse.jface.text.presentation.PresentationReconciler;
@@ -14,20 +23,29 @@ import org.eclipse.jface.text.rules.DefaultDamagerRepairer; 
import org.eclipse.jface.text.rules.Token;

import org.eclipse.jface.text.source.IAnnotationHover;

import org.eclipse.jface.text.source.ISourceViewer;

import org.eclipse.swt.custom.StyledText;

import org.eclipse.swt.widgets.Composite;

import org.eclipse.swt.widgets.Shell;

import org.eclipse.ui.editors.text.TextSourceViewerConfiguration;

import org.lamport.tla.toolbox.editor.basic.pcal.PCalCompletionProcessor;

import org.lamport.tla.toolbox.editor.basic.pcal.PCalHover;

import org.lamport.tla.toolbox.editor.basic.tla.TLAAnnotationHover;

import org.lamport.tla.toolbox.editor.basic.tla.TLACompletionProcessor;



/**

 * Configuration of the source viewer for TLA+ editor 

 * @author Simon Zambrovski

 * @version $Id$

 */

public class TLASourceViewerConfiguration extends TextSourceViewerConfiguration

{



    private final TLAEditor editor;



	public TLASourceViewerConfiguration() {

		super();

		this.editor = null;

	}



    /**

     * Constructs configuration based on a preference store  

     * @param preferenceStore
@@ -108,12 +126,23 @@ public class TLASourceViewerConfiguration extends TextSourceViewerConfiguration 
     */

    public IContentAssistant getContentAssistant(ISourceViewer sourceViewer)

    {



        ContentAssistant assistant = new ContentAssistant();

        assistant.setDocumentPartitioning(getConfiguredDocumentPartitioning(sourceViewer));

        assistant.setContentAssistProcessor(new TLACompletionProcessor(), IDocument.DEFAULT_CONTENT_TYPE);

        assistant.setContentAssistProcessor(new PCalCompletionProcessor(), TLAPartitionScanner.TLA_PCAL);

        assistant.enableColoredLabels(true);

        assistant.enableAutoActivation(true);

        assistant.setAutoActivationDelay(500);

		assistant.setInformationControlCreator(new IInformationControlCreator() {

			public IInformationControl createInformationControl(final Shell parent) {

				return new DefaultInformationControl(parent, (DefaultInformationControl.IInformationPresenter) null);

			}

		});

		assistant.setSorter(new ICompletionProposalSorter() {

			public int compare(ICompletionProposal p1, ICompletionProposal p2) {

				return 0;

			}

		});

        assistant.setProposalPopupOrientation(IContentAssistant.PROPOSAL_OVERLAY);

        assistant.setContextInformationPopupOrientation(IContentAssistant.CONTEXT_INFO_ABOVE);

        assistant.setContextInformationPopupBackground(TLAEditorActivator.getDefault().getTLAColorProvider().getColor(
@@ -121,6 +150,30 @@ public class TLASourceViewerConfiguration extends TextSourceViewerConfiguration 
        return assistant;

    }



	/* (non-Javadoc)

	 * @see org.eclipse.ui.editors.text.TextSourceViewerConfiguration#getTextHover(org.eclipse.jface.text.source.ISourceViewer, java.lang.String)

	 */

	@Override

	public ITextHover getTextHover(ISourceViewer sourceViewer, String contentType) {

		if (TLAPartitionScanner.TLA_PCAL.equals(contentType)) {

			return new PCalHover();

		}

		return new ToolboxHover();

	}

	

	/* (non-Javadoc)

	 * @see org.eclipse.jface.text.source.SourceViewerConfiguration#getInformationControlCreator(org.eclipse.jface.text.source.ISourceViewer)

	 */

	@Override

	public IInformationControlCreator getInformationControlCreator(ISourceViewer sourceViewer) {

		// We want the hover popup to use a monospaced font.

		return new IInformationControlCreator() {

			public IInformationControl createInformationControl(final Shell parent) {

				return new MonospacedDefaultInformationControl(parent);

			}

		};

	}



    /**

     * Ruler annotation

     */
@@ -156,4 +209,25 @@ public class TLASourceViewerConfiguration extends TextSourceViewerConfiguration 
        return new String[] { "\\*", "" };

    }



    public static class MonospacedDefaultInformationControl extends DefaultInformationControl {

    	public MonospacedDefaultInformationControl(final Shell parent) {

    		super(parent, (DefaultInformationControl.IInformationPresenter) null);

    	}



		@Override

		protected void createContent(Composite parent) {

			super.createContent(parent);

			try {

				final Field f = DefaultInformationControl.class.getDeclaredField("fText");

				f.setAccessible(true);

				final StyledText fText = (StyledText) f.get(this); // IllegalAccessException

				

				fText.setFont(JFaceResources.getFont(JFaceResources.TEXT_FONT));

			} catch (NoSuchFieldException e) {

			} catch (SecurityException e) {

			} catch (IllegalArgumentException e) {

			} catch (IllegalAccessException e) {

			}

		}

    }

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/ToolboxCompletionProcessor.java

0 → 100644
+360 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic;



import java.nio.CharBuffer;

import java.util.ArrayList;

import java.util.Collection;

import java.util.List;

import java.util.SortedMap;

import java.util.TreeMap;



import org.eclipse.core.runtime.Assert;

import org.eclipse.core.runtime.IProgressMonitor;

import org.eclipse.jface.text.BadLocationException;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IRegion;

import org.eclipse.jface.text.ITextViewer;

import org.eclipse.jface.text.contentassist.BoldStylerProvider;

import org.eclipse.jface.text.contentassist.ContextInformation;

import org.eclipse.jface.text.contentassist.ICompletionProposal;

import org.eclipse.jface.text.contentassist.ICompletionProposalExtension5;

import org.eclipse.jface.text.contentassist.ICompletionProposalExtension7;

import org.eclipse.jface.text.contentassist.IContextInformation;

import org.eclipse.jface.text.contentassist.IContextInformationValidator;

import org.eclipse.jface.viewers.StyledString;

import org.eclipse.swt.graphics.Image;

import org.eclipse.swt.graphics.Point;

import org.lamport.tla.toolbox.editor.basic.tla.ITLAReserveredWords;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;

import org.lamport.tla.toolbox.tool.ToolboxHandle;



import tla2sany.modanalyzer.SpecObj;

import tla2sany.semantic.ModuleNode;

import tla2sany.semantic.SymbolMatcher;

import tla2sany.semantic.SymbolNode;

import util.UniqueString;



public abstract class ToolboxCompletionProcessor {

	

    protected final SortedMap<String, List<CompletionProposalTemplate>> proposals = new TreeMap<String, List<CompletionProposalTemplate>>();

    

    protected final SymbolMatcher.NameAndTypeMatcher matcher = new SymbolMatcher.NameAndTypeMatcher();

    

	public ICompletionProposal[] computeCompletionProposals(ITextViewer viewer, int offset) {

		final IDocument document = viewer.getDocument();

		// get the selection range

		final Point selectedRange = viewer.getSelectedRange();



		final List<ICompletionProposal> propList = new ArrayList<ICompletionProposal>();

		try {

			// The zero-based row index of the caret.

			final int caretRowIndex = document.getLineOfOffset(offset);

			// The zero-based column index of the caret.

			final int carretColumnIndex = offset - document.getLineOffset(caretRowIndex);

			if (selectedRange.y > 0) {

				// the range is non-empty

				final String text = document.get(selectedRange.x, selectedRange.y);

				computeWordProposals(text, offset, carretColumnIndex, propList);

			} else {

				// the range is empty, no selection in the editor



				// get the region

				final IRegion wordRegion = DocumentHelper.getRegionExpandedBackwards(document, offset,

						DocumentHelper.getDefaultWordDetector());

				final String word = document.get(wordRegion.getOffset(), wordRegion.getLength());

				computeWordProposals(word, offset, carretColumnIndex, propList);

			}

		} catch (final BadLocationException ignore) {

		}

		return propList.toArray(new ICompletionProposal[propList.size()]);

	}



    /**

     * Syntax-based proposal based for word beginning

     */

	private void computeWordProposals(final String word, final int offset, final int carretColumnIndex, final List<ICompletionProposal> propositionList) {

		final int qualifierLength = word.length();

		final int replacementOffset = offset - qualifierLength;



		// keyword and other static proposals

		for (List<CompletionProposalTemplate> list : filterPrefix(proposals, word).values()) {

			// and add to result list

			for (CompletionProposalTemplate template : list) {

				propositionList.add(template.getProposal(replacementOffset, carretColumnIndex - qualifierLength, qualifierLength));

			}

		}

		

		// Try to find matches among the spec's set of symbols (e.g. operators definitions and declarations).

		final SpecObj specObj = ToolboxHandle.getSpecObj();

		if (specObj != null && specObj.getRootModule() != null) { // null if spec hasn't been parsed.

			final ModuleNode rootModule = specObj.getRootModule();



			final Collection<SymbolNode> symbols = rootModule.getSymbols(matcher.setPrefix(word));

			for (final SymbolNode symbolNode : symbols) {

				propositionList.add(new CompletionProposalTemplate(symbolNode.getSignature(), symbolNode.getName(),

						symbolNode.getHumanReadableImage()).getProposal(replacementOffset, carretColumnIndex - qualifierLength, qualifierLength));

			}

		}

	}

    

	public static SortedMap<String, List<CompletionProposalTemplate>> filterPrefix(SortedMap<String, List<CompletionProposalTemplate>> baseMap, String prefix) {

		if (prefix.length() > 0) {

			final char nextLetter = (char) (prefix.charAt(prefix.length() - 1) + 1);

 			final String end = prefix.substring(0, prefix.length() - 1) + nextLetter;

			return baseMap.subMap(prefix, end);

		}

		return baseMap;

	}



	public IContextInformation[] computeContextInformation(ITextViewer viewer, int offset) {

		// Retrieve selected range

		final Point selectedRange = viewer.getSelectedRange();

		if (selectedRange.y > 0) {

			// Text is selected. Create a context information array.

			final IContextInformation[] contextInfos = new ContextInformation[ITLAReserveredWords.ALL_WORDS_ARRAY.length];



			// Create one context information item for each style

			for (int i = 0; i < ITLAReserveredWords.ALL_WORDS_ARRAY.length; i++) {

				contextInfos[i] = new ContextInformation(null, ITLAReserveredWords.ALL_WORDS_ARRAY[i] + " Style");

			}

			return contextInfos;

		}

		return new ContextInformation[0];

	}



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getCompletionProposalAutoActivationCharacters()

     */

	public char[] getCompletionProposalAutoActivationCharacters() {

		return null;

	}



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getContextInformationAutoActivationCharacters()

     */

	public char[] getContextInformationAutoActivationCharacters() {

		return null;

	}



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getContextInformationValidator()

     */

	public IContextInformationValidator getContextInformationValidator() {

		return null;

	}



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getErrorMessage()

     */

	public String getErrorMessage() {

		return null;

	}

	

	protected static class CompletionProposalTemplate {

		private final String fReplacementString;

		private final Image fImage;

		private final IContextInformation fContextInformation;

		private final String fAdditionalProposalInfo;

		private final String fDisplayString;

		

		public CompletionProposalTemplate(String replacementString, Image image, String dipslayString,

				IContextInformation contextInformation, String additionalProposalInfo) {

			this.fReplacementString = replacementString;

			this.fImage = image;

			this.fDisplayString = dipslayString;

			this.fContextInformation = contextInformation;

			this.fAdditionalProposalInfo = additionalProposalInfo;

		}

		

		public CompletionProposalTemplate(String replacementString, Image image, String dipslayString,

				String additionalProposalInfo) {

			this.fReplacementString = replacementString;

			this.fImage = image;

			this.fDisplayString = dipslayString;

			this.fContextInformation = null;

			this.fAdditionalProposalInfo = additionalProposalInfo;

		}

		

		public CompletionProposalTemplate(UniqueString replacementString, UniqueString dipslayString,

				String additionalProposalInfo) {

			this(replacementString.toString(), dipslayString.toString(), additionalProposalInfo);

		}

		

		public CompletionProposalTemplate(String replacementString, UniqueString dipslayString,

				String additionalProposalInfo) {

			this(replacementString, dipslayString.toString(), additionalProposalInfo);

		}

		

		public CompletionProposalTemplate(String replacementString, String dipslayString,

				String additionalProposalInfo) {

			this.fReplacementString = replacementString;

			this.fImage = null;

			this.fDisplayString = dipslayString;

			this.fContextInformation = null;

			this.fAdditionalProposalInfo = additionalProposalInfo;

		}

		

		public CompletionProposalTemplate(String replacementString) {

			this.fReplacementString = replacementString;

			this.fImage = null; // Image for keywords?!

			this.fContextInformation = null;

			this.fAdditionalProposalInfo = null;

			this.fDisplayString = null;

		}



		public ICompletionProposal getProposal(final int replacementOffset, final int wordStartColumnIndex, final int qualifierLength) {

			final String indent = CharBuffer.allocate(wordStartColumnIndex).toString().replace( '\0', ' ' );

			final String indentedReplacementString = fReplacementString.replace("\n", "\n" + indent);

			return new ToolboxCompletionProposal(indentedReplacementString, replacementOffset, qualifierLength,

					indentedReplacementString.length(), fImage, fDisplayString, fContextInformation,

					fAdditionalProposalInfo);

		}

	}

	

	public static class ToolboxCompletionProposal implements ICompletionProposal, ICompletionProposalExtension5, ICompletionProposalExtension7 {



		/** The string to be displayed in the completion proposal popup. */

		private String fDisplayString;

		/** The replacement string. */

		private String fReplacementString;

		/** The replacement offset. */

		private int fReplacementOffset;

		/** The replacement length. */

		private int fReplacementLength;

		/** The cursor position after this proposal has been applied. */

		private int fCursorPosition;

		/** The image to be displayed in the completion proposal popup. */

		private Image fImage;

		/** The context information of this proposal. */

		private IContextInformation fContextInformation;

		/** The additional info of this proposal. */

		private String fAdditionalProposalInfo;



		/**

		 * Creates a new completion proposal based on the provided information. The

		 * replacement string is considered being the display string too. All remaining

		 * fields are set to <code>null</code>.

		 *

		 * @param replacementString

		 *            the actual string to be inserted into the document

		 * @param replacementOffset

		 *            the offset of the text to be replaced

		 * @param replacementLength

		 *            the length of the text to be replaced

		 * @param cursorPosition

		 *            the position of the cursor following the insert relative to

		 *            replacementOffset

		 */

		public ToolboxCompletionProposal(String replacementString, int replacementOffset, int replacementLength,

				int cursorPosition) {

			this(replacementString, replacementOffset, replacementLength, cursorPosition, null, null, null, null);

		}



		/**

		 * Creates a new completion proposal. All fields are initialized based on the

		 * provided information.

		 *

		 * @param replacementString

		 *            the actual string to be inserted into the document

		 * @param replacementOffset

		 *            the offset of the text to be replaced

		 * @param replacementLength

		 *            the length of the text to be replaced

		 * @param cursorPosition

		 *            the position of the cursor following the insert relative to

		 *            replacementOffset

		 * @param image

		 *            the image to display for this proposal

		 * @param displayString

		 *            the string to be displayed for the proposal

		 * @param contextInformation

		 *            the context information associated with this proposal

		 * @param additionalProposalInfo

		 *            the additional information associated with this proposal

		 */

		public ToolboxCompletionProposal(String replacementString, int replacementOffset, int replacementLength,

				int cursorPosition, Image image, String displayString, IContextInformation contextInformation,

				String additionalProposalInfo) {

			Assert.isNotNull(replacementString);

			Assert.isTrue(replacementOffset >= 0);

			Assert.isTrue(replacementLength >= 0);

			Assert.isTrue(cursorPosition >= 0);



			fReplacementString = replacementString;

			fReplacementOffset = replacementOffset;

			fReplacementLength = replacementLength;

			fCursorPosition = cursorPosition;

			fImage = image;

			fDisplayString = displayString;

			fContextInformation = contextInformation;

			fAdditionalProposalInfo = additionalProposalInfo;

		}



		public void apply(IDocument document) {

			try {

				document.replace(fReplacementOffset, fReplacementLength, fReplacementString);

			} catch (BadLocationException x) {

				// ignore

			}

		}



		public Point getSelection(IDocument document) {

			return new Point(fReplacementOffset + fCursorPosition, 0);

		}



		public IContextInformation getContextInformation() {

			return fContextInformation;

		}



		public Image getImage() {

			return fImage;

		}



		public String getDisplayString() {

			if (fDisplayString != null)

				return fDisplayString;

			return fReplacementString;

		}



		public String getAdditionalProposalInfo() {

			return fAdditionalProposalInfo;

		}



		public Object getAdditionalProposalInfo(IProgressMonitor monitor) {

			return getAdditionalProposalInfo();

		}



		public StyledString getStyledDisplayString(IDocument document, int offset,

				BoldStylerProvider boldStylerProvider) {

			final StyledString styledString = new StyledString();

			styledString.append(getDisplayString());

			styledString.append(": ");

			styledString.append(fReplacementString.replaceAll("\n[ ]*", " "), StyledString.COUNTER_STYLER);

			return styledString;

		}

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/ToolboxHover.java

0 → 100644
+87 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic;



import org.eclipse.jface.text.BadLocationException;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IRegion;

import org.eclipse.jface.text.ITextHover;

import org.eclipse.jface.text.ITextViewer;

import org.eclipse.jface.text.Region;

import org.lamport.tla.toolbox.editor.basic.pcal.PCalWordDetector;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;

import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper.WordRegion;

import org.lamport.tla.toolbox.tool.ToolboxHandle;



import tla2sany.modanalyzer.SpecObj;

import tla2sany.semantic.SymbolNode;



public class ToolboxHover implements ITextHover {

	

	/* (non-Javadoc)

	 * @see org.eclipse.jface.text.ITextHover#getHoverInfo(org.eclipse.jface.text.ITextViewer, org.eclipse.jface.text.IRegion)

	 */

	public String getHoverInfo(ITextViewer textViewer, IRegion hoverRegion) {

		// Expand the given region to word (token) and get the token. If it can't get

		// the token, no hover help is provided.

		final WordRegion wordRegion;

		try {

			wordRegion = DocumentHelper.getRegionExpandedBoth(textViewer.getDocument(),

					hoverRegion.getOffset(), new PCalWordDetector());

		} catch (BadLocationException ignore) {

			return null;

		}



		final String hoverInfo = getHoverInfo(textViewer.getDocument(), wordRegion);

		if (hoverInfo != null) {

			return hoverInfo;

		}



		// No keywords, lets look for operator definitions. For that, the spec has to be

		// in parsed state.

		final SpecObj spec = ToolboxHandle.getSpecObj();

		if (spec != null) { // null if spec hasn't been parsed.

			final SymbolNode symbol = EditorUtil.lookupSymbol(spec, textViewer.getDocument(), wordRegion);

			if (symbol == null) {

				return null;

			}

			return symbol.getHumanReadableImage();

		}

		return null;

	}

	

	protected String getHoverInfo(IDocument document, WordRegion wordRegion) {

		return null;

	}



	/* (non-Javadoc)

	 * @see org.eclipse.jface.text.ITextHover#getHoverRegion(org.eclipse.jface.text.ITextViewer, int)

	 */

	public IRegion getHoverRegion(ITextViewer textViewer, int offset) {

		return new Region(offset, 0);

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/actions/ExampleEditorAction.java

+1 −2
Original line number Diff line number Diff line
@@ -67,10 +67,9 @@ public class ExampleEditorAction extends TextEditorAction implements VerifyKeyLi 


                    // retrieve the region describing the word containing

                    // the caret

                    IRegion region = DocumentHelper.getRegionExpandedBoth(document, textSelection.getOffset(),

                            DocumentHelper.getDefaultWordDetector());

                    try

                    {

                    	IRegion region = DocumentHelper.getRegionExpandedBoth(document, textSelection.getOffset());



                        // generate the insertion string

                        String insertionText = " " + document.get(region.getOffset(), region.getLength());

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/actions/OpenDeclarationAction.java

+17 −46
Original line number Diff line number Diff line 
package org.lamport.tla.toolbox.editor.basic.actions;



import org.eclipse.core.resources.IFile;

import org.eclipse.core.resources.IResource;

import org.eclipse.core.runtime.IStatus;

import org.eclipse.core.runtime.Status;

import org.eclipse.jface.action.Action;

import org.eclipse.jface.text.IRegion;

import org.eclipse.jface.text.ITextSelection;

import org.eclipse.jface.text.hyperlink.IHyperlink;

import org.eclipse.jface.viewers.ISelection;

import org.eclipse.ui.part.FileEditorInput;

import org.eclipse.ui.IEditorInput;

import org.eclipse.ui.IEditorPart;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;

import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;

import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;

import org.lamport.tla.toolbox.spec.Spec;

import org.lamport.tla.toolbox.tool.ToolboxHandle;

import org.lamport.tla.toolbox.util.UIHelper;



/**
@@ -29,58 +21,38 @@ import org.lamport.tla.toolbox.util.UIHelper; 
 * nested class.

 * 

 * @author Simon Zambrovski

 * @version $Id$

 */

public class OpenDeclarationAction extends Action implements IHyperlink

{

    private IResource resource;

    private IRegion location;

    private String label;

    private final IEditorInput editorInput;

    private final IRegion location;

    private final String label;

    private final IRegion hyperlinkLocation;

	private final String editorId;



    /**

     * Constructs the action

     * @param targetResource resource to link

     * @param targetLocation location in the resource

     * @param hyperlinkLabel label of the hyperlink

     * @param hyperlinkLocation location of the hyperlink

     */

    public OpenDeclarationAction(IResource targetResource, IRegion targetLocation, String hyperlinkLabel,

    public OpenDeclarationAction(String editorId, IEditorInput editorInput, IRegion targetLocation, String hyperlinkLabel,

            IRegion hyperlinkLocation)

    {

        super();

        this.resource = targetResource;

		this.editorId = editorId;

        this.editorInput = editorInput;

        this.location = targetLocation;

        this.label = hyperlinkLabel;

        this.hyperlinkLocation = hyperlinkLocation;

    }



    /**

     * Action method  

    /* (non-Javadoc)

     * @see org.eclipse.jface.action.Action#run()

     */

    public void run()

    {

		TLAEditorActivator

				.getDefault()

				.getLog()

				.log(new Status(IStatus.INFO, TLAEditorActivator.PLUGIN_ID,

						"Opening " + label + "(" + resource.getName() + " at "

								+ location + ")"));

        EditorUtil.setReturnFromOpenDecl();

//        // Find current location and store as a property of the spec for the

//        // Return from Goto Declaration command.

//        TLAEditor srcEditor = EditorUtil.getTLAEditorWithFocus();

//        if (srcEditor != null)

//        {

//            Spec spec = ToolboxHandle.getCurrentSpec();

//            spec.setOpenDeclModuleName(srcEditor.getEditorInput().getName());

//            spec.setOpenDeclSelection((ITextSelection) srcEditor.getSelectionProvider().getSelection());

//        }



        TLAEditorAndPDFViewer editor = (TLAEditorAndPDFViewer) UIHelper.openEditor(TLAEditorAndPDFViewer.ID,

                new FileEditorInput((IFile) resource));

        editor.getTLAEditor().selectAndReveal(location.getOffset(), location.getLength());



        final IEditorPart editor = UIHelper.openEditor(editorId, editorInput);

        if (editor instanceof TLAEditorAndPDFViewer) {

        	((TLAEditorAndPDFViewer) editor).getTLAEditor().selectAndReveal(location.getOffset(), location.getLength());

        } else if (editor instanceof TLAEditor) {

        	((TLAEditor) editor).selectAndReveal(location.getOffset(), location.getLength());

        }

    }



    /* (non-Javadoc)
@@ -114,5 +86,4 @@ public class OpenDeclarationAction extends Action implements IHyperlink 
    {

        run();

    }



}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/ExampleEditCommandHandler.java

+2 −4
Original line number Diff line number Diff line
@@ -16,7 +16,6 @@ import org.eclipse.swt.events.VerifyEvent; 
import org.lamport.tla.toolbox.Activator;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;

import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;



/**

 * Performs a useless command to illustrate how to get keyboard input
@@ -125,10 +124,9 @@ public class ExampleEditCommandHandler extends AbstractHandler implements Verify 


                        // retrieve the region describing the word containing

                        // the caret

                        IRegion region = DocumentHelper.getRegionExpandedBoth(document, textSelection.getOffset(),

                                DocumentHelper.getDefaultWordDetector());

                        try

                        {

                        	IRegion region = DocumentHelper.getRegionExpandedBoth(document, textSelection.getOffset());



                            // generate the insertion string

                            String insertionText = " " + document.get(region.getOffset(), region.getLength());
@@ -186,7 +184,7 @@ public class ExampleEditCommandHandler extends AbstractHandler implements Verify 
     * This is added as a focus listener so that it can uninstall()

     * itself if focus is lost.

     */

    private void install()

    public void install()

    {

        editor.getViewer().prependVerifyKeyListener(this);

        editor.getViewer().getTextWidget().addFocusListener(this);

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/PCalTranslateAutomaticallyHandler.java

0 → 100644
+98 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic.handlers;



import java.lang.reflect.InvocationTargetException;



import javax.inject.Inject;



import org.eclipse.core.commands.Command;

import org.eclipse.core.commands.ExecutionEvent;

import org.eclipse.core.commands.ExecutionException;

import org.eclipse.core.commands.State;

import org.eclipse.core.runtime.Assert;

import org.eclipse.e4.core.di.annotations.Execute;

import org.eclipse.e4.core.services.events.IEventBroker;

import org.eclipse.ui.IWorkbench;

import org.eclipse.ui.commands.ICommandService;

import org.eclipse.ui.handlers.HandlerUtil;

import org.eclipse.ui.handlers.RegistryToggleState;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.editor.basic.pcal.PCalTranslator;

import org.osgi.service.event.Event;

import org.osgi.service.event.EventHandler;



public class PCalTranslateAutomaticallyHandler extends PCalTranslator implements EventHandler {



	@Inject

	public void initializeAtStartup(final IWorkbench workbench, final ICommandService commandService) {

		/*

		 * Check the UI state of the IHandler/Command which indicates if the user

		 * enabled automatic PlusCal conversion.

		 */

		final Command command = commandService.getCommand("toolbox.command.module.translate.automatially");

		final State state = command.getState(RegistryToggleState.STATE_ID);

		if (!((Boolean) state.getValue()).booleanValue()) {

			return;

		}

		// This IHander is stateful even across Toolbox restarts. In other words, if the

		// user enables automatic PlusCal translation, it will remain enabled even after

		// a Toolbox restart. This means we have to register this EventHandler at the

		// IEventBroker during Toolbox startup.

		// It is vital that we use the Workbench's IEventBroker instance. If e.g. we

		// would use an IEventBroker from higher up the IEclipseContext hierarchy, the

		// broker would be disposed when a new spec gets opened while the IHandler's state

		// remains enabled.

		workbench.getService(IEventBroker.class).unsubscribe(this);

		Assert.isTrue(workbench.getService(IEventBroker.class).subscribe(TLAEditor.PRE_SAVE_EVENT, this));

	}

	

	@Execute

	public void execute(final ExecutionEvent event, final IWorkbench workbench) throws ExecutionException {

		// Toggle the IHandler's state at the UI level (check mark on/off) and

		// unsubscribe/subscribe the EventHandler.

		final IEventBroker eventBroker = workbench.getService(IEventBroker.class);

		if (HandlerUtil.toggleCommandState(event.getCommand())) {

			eventBroker.unsubscribe(this);

		} else {

			eventBroker.unsubscribe(this);

			Assert.isTrue(eventBroker.subscribe(TLAEditor.PRE_SAVE_EVENT, this));

		}

	}

	

	/* (non-Javadoc)

	 * @see org.osgi.service.event.EventHandler#handleEvent(org.osgi.service.event.Event)

	 */

	@Override

	public void handleEvent(final Event event) {

		try {

			final TLAEditor editor = (TLAEditor) event.getProperty(IEventBroker.DATA);

			translate(editor, editor.getSite().getShell(), false);

		} catch (InvocationTargetException | InterruptedException e) {

			throw new RuntimeException(e);

		}

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/PCalTranslateModuleHandler.java

0 → 100644
+76 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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:

 *   Simon Zambrowski - initial API and implementation

 *   Markus Alexander Kuppe - Refactoring

 ******************************************************************************/

package org.lamport.tla.toolbox.editor.basic.handlers;



import java.lang.reflect.InvocationTargetException;



import org.eclipse.core.commands.ExecutionEvent;

import org.eclipse.core.commands.ExecutionException;

import org.eclipse.ui.IEditorPart;

import org.eclipse.ui.handlers.HandlerUtil;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;

import org.lamport.tla.toolbox.editor.basic.pcal.PCalTranslator;

import org.lamport.tla.toolbox.ui.handler.SaveDirtyEditorAbstractHandler;



/**

 * Triggers the PCal translation of the module

 * 

 * @author Simon Zambrovski

 */

public class PCalTranslateModuleHandler extends SaveDirtyEditorAbstractHandler {



	public Object execute(final ExecutionEvent event) throws ExecutionException {

		if (!saveDirtyEditor(event)) {

			// Cannot translate a dirty editor.

			return null;

		}

		final TLAEditor tlaEditor = getTLAEditor(activeEditor);

		if (tlaEditor == null || !tlaEditor.hasPlusCal()) {

			// If it's not a TLAEditor, it can't have PlusCal code.

			return null;

		}



		try {

			new PCalTranslator().translate(tlaEditor, HandlerUtil.getActiveShell(event));

		} catch (InvocationTargetException | InterruptedException e) {

			throw new ExecutionException(e.getMessage(), e);

		}

		return null;

	}

	

	private static TLAEditor getTLAEditor(IEditorPart anEditor) {

		if (anEditor instanceof TLAEditorAndPDFViewer) {

			final TLAEditorAndPDFViewer editor = (TLAEditorAndPDFViewer) anEditor;

			return editor.getTLAEditor();

		}

		if (anEditor instanceof TLAEditor) {

			return (TLAEditor) anEditor;

		}

		return null;

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/handlers/ShowDeclarationsHandler.java

+59 −64
Original line number Diff line number Diff line
@@ -3,8 +3,9 @@ 
 */

package org.lamport.tla.toolbox.editor.basic.handlers;



import java.util.Arrays;

import java.util.Vector;

import java.util.Collection;

import java.util.HashSet;

import java.util.Set;



import org.eclipse.core.commands.AbstractHandler;

import org.eclipse.core.commands.ExecutionEvent;
@@ -25,8 +26,13 @@ import org.lamport.tla.toolbox.editor.basic.util.EditorUtil; 
import org.lamport.tla.toolbox.util.ResourceHelper;

import org.lamport.tla.toolbox.util.UIHelper;



import tla2sany.semantic.ASTConstants;

import tla2sany.semantic.AnyDefNode;

import tla2sany.semantic.ModuleNode;

import tla2sany.semantic.OpDeclNode;

import tla2sany.semantic.OpDefNode;

import tla2sany.semantic.SemanticNode;

import tla2sany.semantic.SymbolMatcher;

import tla2sany.semantic.SymbolNode;

import tla2sany.semantic.ThmOrAssumpDefNode;
@@ -118,6 +124,48 @@ public class ShowDeclarationsHandler extends AbstractHandler implements IHandler 


        // int curSelection; // The currently selected item.



		private final SymbolMatcher.NameAndTypeMatcher matcher = new SymbolMatcher.NameAndTypeMatcher() {



			/* (non-Javadoc)

			 * @see tla2sany.semantic.SymbolMatcher.NameAndTypeMatcher#matchTypes()

			 */

			@Override

			public Set<Class<? extends SymbolNode>> matchTypes() {

				final Set<Class<? extends SymbolNode>> set = new HashSet<Class<? extends SymbolNode>>();

				set.add(OpDefNode.class);

				set.add(OpDeclNode.class);

				set.add(ThmOrAssumpDefNode.class);

				return set;

			}



			/* (non-Javadoc)

			 * @see tla2sany.semantic.SymbolMatcher.NameAndTypeMatcher#matches(tla2sany.semantic.SymbolNode)

			 */

			@Override

			public boolean matches(SymbolNode aSymbol) {

				if (aSymbol instanceof ThmOrAssumpDefNode || aSymbol instanceof OpDefNode) {

					if (aSymbol.getKind() == ASTConstants.ModuleInstanceKind) {

						// Do not match INSTANCE symbols, e.g.: "InChan" defined as:

						// InChan  == INSTANCE Channel WITH ...

						return false;

					}

					if (aSymbol.getKind() == ASTConstants.BuiltInKind) {

						// Do not match built-in operators.

						return false;

					}

					if (!ResourceHelper.isFromUserModule((SemanticNode) ((AnyDefNode) aSymbol).getSource())) {

						// Do not match symbols of the Standard Modules such as Sequences, FiniteSets...

						return false;

					}

					if (!showAll && (((AnyDefNode) aSymbol).getSource() != aSymbol)) {

						// Unless showAll, do not match symbols defined or declared by extended modules. 

						return false;

					}

				}

				return super.matches(aSymbol);

			}

		};

        

        /**

         * Constructs a new Show Declarations popup with indicated parent and

         * with showAll determining if instantiated definitions should be shown.
@@ -142,8 +190,6 @@ public class ShowDeclarationsHandler extends AbstractHandler implements IHandler 
            {

                module = ResourceHelper.getModuleNode(editor.getModuleName());

            }

            System.out.println("Created new popup with showAll = " + showAll);



        }



        /**
@@ -173,71 +219,20 @@ public class ShowDeclarationsHandler extends AbstractHandler implements IHandler 
         */

        protected void setList()

        {

            // Get the list of SymbolNodes to be displayed. They

            // come from the module's constant decls, variable decls,

            // opdef nodes, ThmOrAssumpDefNodes.



            String lcFilterPrefix = filterPrefix.toLowerCase();

            list.removeAll();

            // Get the current module.

            if (module == null)

            {

                return;

            }

            Vector symVec = new Vector(40);

            SymbolNode[] syms = module.getConstantDecls();

            for (int i = 0; i < syms.length; i++)

            {

                if (syms[i].getName().toString().toLowerCase().startsWith(lcFilterPrefix))

                {

                    symVec.add(syms[i]);

                }

            }

            

            syms = module.getVariableDecls();

            for (int i = 0; i < syms.length; i++)

            {

                if (syms[i].getName().toString().toLowerCase().toLowerCase().startsWith(lcFilterPrefix))

                {

                    symVec.add(syms[i]);

                }

            }



            OpDefNode[] symsOpD = module.getOpDefs();

            for (int i = 0; i < symsOpD.length; i++)

            {

                if (ResourceHelper.isFromUserModule(symsOpD[i].getSource())

                        && (showAll || (symsOpD[i].getSource() == symsOpD[i]))

                        && symsOpD[i].getName().toString().toLowerCase().startsWith(lcFilterPrefix))

                {

                    symVec.add(symsOpD[i]);

                }

            }



            ThmOrAssumpDefNode[] symsTAD = module.getThmOrAssDefs();

            for (int i = 0; i < symsTAD.length; i++)

            {

                if (ResourceHelper.isFromUserModule(symsTAD[i].getSource())

                        && (showAll || (symsTAD[i].getSource() == symsTAD[i]))

                        && symsTAD[i].getName().toString().toLowerCase().startsWith(lcFilterPrefix))

                {

                    symVec.add(symsTAD[i]);

                }

            }



            SymbolNode[] symbols = new SymbolNode[symVec.size()];



            for (int i = 0; i < symbols.length; i++)

            {

                symbols[i] = (SymbolNode) symVec.get(i);

            }



            Arrays.sort(symbols);



            for (int i = 0; i < symbols.length; i++)

            {

                list.add(symbols[i].getName().toString());

                list.setData(symbols[i].getName().toString(), symbols[i]);

            // Get the list of SymbolNodes to be displayed. They

            // come from the module's constant decls, variable decls,

            // opdef nodes, ThmOrAssumpDefNodes.

            final Collection<SymbolNode> symbols = module.getSymbols(matcher.setPrefix(filterPrefix.toLowerCase()));

            for (SymbolNode symbolNode : symbols) {

                list.add(symbolNode.getName().toString());

                list.setData(symbolNode.getName().toString(), symbolNode);

			}

        }

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalCompletionProcessor.java

0 → 100644
+91 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic.pcal;



import java.util.ArrayList;

import java.util.List;



import org.eclipse.jface.text.contentassist.IContentAssistProcessor;

import org.lamport.tla.toolbox.editor.basic.ToolboxCompletionProcessor;



public class PCalCompletionProcessor extends ToolboxCompletionProcessor implements IContentAssistProcessor {



	public PCalCompletionProcessor() {

		// No sense to add "--algorithm" because the 'PCalCompletionProcessor is only

		// hot when cursor/caret inside a PCal algorithm. Thus "--algorithm" is part of

		// TLACompletionProcessor.

//    	proposals.put(IPCalReservedWords.ALGORITHM, "--algorithm AName {\n}");

    	

		List<CompletionProposalTemplate> templates = new ArrayList<CompletionProposalTemplate>();

		templates.add(new CompletionProposalTemplate("process (ProcName \\in S) {\n     label: skip;\n}", 

				IPCalReservedWords.PROCESS, IPCalReservedWords.PROCESS_HELP));

		templates.add(new CompletionProposalTemplate("process (ProcName = Id) {\n    label: skip;\n}",

				IPCalReservedWords.PROCESS, IPCalReservedWords.PROCESS_HELP));

		proposals.put(IPCalReservedWords.PROCESS, templates);



		templates = new ArrayList<ToolboxCompletionProcessor.CompletionProposalTemplate>();

		templates.add(

				new CompletionProposalTemplate("if (TRUE) {\n   skip;\n};", "if-then", IPCalReservedWords.IFTHENELSE_HELP));

		templates.add(new CompletionProposalTemplate("if (TRUE) {\n   skip;\n} else {\n   skip;\n};", "if-then-else",

				IPCalReservedWords.IFTHENELSE_HELP));

		templates.add(new CompletionProposalTemplate("if (TRUE) {\n   skip;\n} else if (FALSE) {\n   skip;\n} else {\n   skip;\n};", "if-then-elseif",

				IPCalReservedWords.IFTHENELSE_HELP));

		proposals.put(IPCalReservedWords.IF, templates);



		proposals.put(IPCalReservedWords.VARIABLE,

				getSingleProposal("variable x = TRUE;", IPCalReservedWords.VARIABLE, IPCalReservedWords.VARIABLE_HELP));

		proposals.put(IPCalReservedWords.VARIABLES, getSingleProposal("variables x = TRUE;\n          y \\in {1,2,3};\n          z;",

				IPCalReservedWords.VARIABLES, IPCalReservedWords.VARIABLE_HELP));

		proposals.put(IPCalReservedWords.PROCEDURE,

				getSingleProposal("procedure PName (param1, ..., paramN) {\n  label: skip;\n}", IPCalReservedWords.PROCEDURE,

						IPCalReservedWords.PROCEDURE_HELP));

		proposals.put(IPCalReservedWords.CALL, getSingleProposal("call PName (expr1, ..., exprN)",

				IPCalReservedWords.CALL, IPCalReservedWords.PROCEDURE_HELP));

		proposals.put(IPCalReservedWords.WHILE, getSingleProposal("label: while (TRUE) {\n         skip;\n};",

				IPCalReservedWords.WHILE, IPCalReservedWords.WHILE_HELP));

		proposals.put(IPCalReservedWords.EITHER, getSingleProposal("either { skip; } or { skip; } or { skip; };",

				IPCalReservedWords.EITHER, IPCalReservedWords.EITHEROR_HELP));

		proposals.put(IPCalReservedWords.ASSERT,

				getSingleProposal("assert TRUE;", IPCalReservedWords.ASSERT, IPCalReservedWords.ASSERT_HELP));

		proposals.put(IPCalReservedWords.GOTO,

				getSingleProposal("goto label;", IPCalReservedWords.GOTO, IPCalReservedWords.GOTO_HELP));

		proposals.put(IPCalReservedWords.PRINT,

				getSingleProposal("print \"msg\";", IPCalReservedWords.PRINT, IPCalReservedWords.PRINT_HELP));

		proposals.put(IPCalReservedWords.WITH, getSingleProposal("with ( i \\in S ) {\n  skip;\n}",

				IPCalReservedWords.WITH, IPCalReservedWords.WITH_HELP));

		proposals.put(IPCalReservedWords.MACRO, getSingleProposal("macro P(param1, ... , paramN) {\n     skip;\n}",

				IPCalReservedWords.MACRO, IPCalReservedWords.MACRO_HELP));

		proposals.put(IPCalReservedWords.DEFINE,

				getSingleProposal("define {\n    Op1(param1, ... , paramN) == TRUE\n    Op2(...) == TRUE\n}",

						IPCalReservedWords.DEFINE, IPCalReservedWords.DEFINE_HELP));

	}

	

	private static List<CompletionProposalTemplate> getSingleProposal(String replacementString, String displayString, String additionalInformation) {

		final List<CompletionProposalTemplate> proposal = new ArrayList<CompletionProposalTemplate>();

		proposal.add(new CompletionProposalTemplate(replacementString, displayString, additionalInformation));

		return proposal;

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalHover.java

0 → 100644
+78 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic.pcal;



import java.util.HashMap;

import java.util.Map;



import org.eclipse.jface.text.IDocument;

import org.lamport.tla.toolbox.editor.basic.ToolboxHover;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper.WordRegion;



public class PCalHover extends ToolboxHover implements IPCalReservedWords {

	

	private final Map<String, String> keywordHover = new HashMap<String, String>();



	public PCalHover() {

		keywordHover.put(ALGORITHM, ALGORITHM_HELP);

		keywordHover.put("algorithm", ALGORITHM_HELP);

		keywordHover.put(DEFINE, DEFINE_HELP);

		keywordHover.put(MACRO, MACRO_HELP);

		keywordHover.put(PROCEDURE, PROCEDURE_HELP);

		keywordHover.put(RETURN, RETURN_HELP);

		keywordHover.put(CALL, CALL_HELP);

		keywordHover.put(PROCESS, PROCESS_HELP);

		keywordHover.put(WHILE, WHILE_HELP);

		keywordHover.put("variable", VARIABLE_HELP);

		keywordHover.put("variables", VARIABLE_HELP);

		keywordHover.put(IF, IFTHENELSE_HELP);

		keywordHover.put(THEN, IFTHENELSE_HELP);

		keywordHover.put(ELSE, IFTHENELSE_HELP);

		keywordHover.put(ELSEIF, IFTHENELSE_HELP);

		keywordHover.put(EITHER, EITHEROR_HELP);

		keywordHover.put(OR, EITHEROR_HELP);

		keywordHover.put(WITH, WITH_HELP);

		keywordHover.put(AWAIT, AWAIT_HELP);

		keywordHover.put(PRINT, PRINT_HELP);

		keywordHover.put(ASSERT, ASSERT_HELP);

		keywordHover.put(SKIP, SKIP_HELP);

		keywordHover.put(GOTO, GOTO_HELP);

		keywordHover.put(":=", ASSIGN_HELP);

		keywordHover.put("||", MULTI_ASSIGN_HELP);

	}



	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.editor.basic.ToolboxHover#getHoverInfo(org.eclipse.jface.text.IDocument, org.lamport.tla.toolbox.editor.basic.util.DocumentHelper.WordRegion)

	 */

	@Override

	protected String getHoverInfo(final IDocument document, final WordRegion wordRegion) {

		// Check if word matches any keywords.

		if (keywordHover.containsKey(wordRegion.getWord())) {

			return keywordHover.get(wordRegion.getWord());

		}

		return null;

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalTranslator.java

0 → 100644
+125 −0
Original line number Diff line number Diff line 
/*******************************************************************************

 * Copyright (c) 2018 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 org.lamport.tla.toolbox.editor.basic.pcal;



import java.lang.reflect.InvocationTargetException;

import java.util.ArrayList;

import java.util.Arrays;

import java.util.List;



import org.eclipse.core.resources.IFile;

import org.eclipse.core.resources.IMarker;

import org.eclipse.core.runtime.IProgressMonitor;

import org.eclipse.jface.dialogs.ProgressMonitorDialog;

import org.eclipse.jface.operation.IRunnableContext;

import org.eclipse.jface.operation.IRunnableWithProgress;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.viewers.ISelection;

import org.eclipse.swt.widgets.Shell;

import org.eclipse.ui.IEditorInput;

import org.eclipse.ui.part.FileEditorInput;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.spec.Spec;

import org.lamport.tla.toolbox.tool.ToolboxHandle;

import org.lamport.tla.toolbox.util.TLAMarkerHelper;

import org.lamport.tla.toolbox.util.UIHelper;

import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;

import org.lamport.tla.toolbox.util.pref.PreferenceStoreHelper;



import pcal.Translator;



public class PCalTranslator {

	

	public void translate(final TLAEditor tlaEditor, final Shell shell) throws InvocationTargetException, InterruptedException {

		translate(tlaEditor, shell, true);	

	}

	

	public void translate(final TLAEditor tlaEditor, final Shell shell, final boolean saveEditor) throws InvocationTargetException, InterruptedException {

		// Running the PlusCal translator takes too long for the UI thread. Thus, the

		// call to the PlusCal translator call is forked off into a non-UI thread.

		// However, we use a ProgressMonitorDialog to lock the UI from further

		// modifications.

		final IRunnableContext context = new ProgressMonitorDialog(tlaEditor.getEditorSite().getShell());

		context.run(true, false, new IRunnableWithProgress() {

			public void run(final IProgressMonitor progressMonitor) throws InvocationTargetException, InterruptedException {

				final IEditorInput editorInput = tlaEditor.getEditorInput();

				final IDocument doc = tlaEditor.getDocumentProvider().getDocument(editorInput);

				final IFile file = ((FileEditorInput) editorInput).getFile();



				final Spec spec = ToolboxHandle.getCurrentSpec();



				// Remove all old markers that indicated parser problems in the previous version

				// of the editor.

				TLAMarkerHelper.removeProblemMarkers(file, progressMonitor,

						TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);



				// Get the user-defined, per spec translator arguments. In almost all cases this

				// is "-nocfg".

				final List<String> asList = new ArrayList<String>(

						Arrays.asList(PreferenceStoreHelper.getStringArray(spec,

								IPreferenceConstants.PCAL_CAL_PARAMS, new String[] { "-nocfg" })));

				// Add the name of the current file to the arguments. The Translator expects

				// this even though we invoke the translator in a way that it doesn't write files.

				asList.add(file.getLocation().toOSString());



				// Run the Translator on the input and check if it succeeded. If it didn't

				// succeed, we know there are parser problems which we will use to marker the

				// editor.

				final Translator translator = new Translator(doc.get(), asList);

				if (translator.translate()) {

					// Update the mapping to/from TLA+ to PlusCal.

					spec.setTpMapping(translator.getMapping(), file.getName(), progressMonitor);



					// User might have edited a non-PlusCal part of the editor. In this case, don't

					// change the editor to not create a superfluous undo operation.

					if (translator.hasChanged()) { 

						// Join the UI thread to modify the editor's content.

						UIHelper.runUISync(new Runnable() {

							public void run() {

								// Replace the documents content while preserving the current caret position.

								final ISelection selection = tlaEditor.getViewer().getSelection();

								doc.set(translator.getOutput());

								tlaEditor.getViewer().setSelection(selection);

	

								// Finally save the editor.

								if (tlaEditor.isDirty() && saveEditor) {

									tlaEditor.doSave(progressMonitor);

								}

							}

						});

					}

				} else {

					// Add parser problem markers to the editor.

					for (Translator.Error anError : translator.getErrors()) {

						TLAMarkerHelper.installProblemMarker(file, file.getName(), IMarker.SEVERITY_ERROR,

								anError.getLocation(), anError.toString(), progressMonitor,

								TLAMarkerHelper.TOOLBOX_MARKERS_TRANSLATOR_MARKER_ID);

					}

				}

			}

		});

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/pcal/PCalWordDetector.java

0 → 100644
+22 −0
Original line number Diff line number Diff line 
package org.lamport.tla.toolbox.editor.basic.pcal;



import org.eclipse.jface.text.rules.IWordDetector;

import org.lamport.tla.toolbox.editor.basic.tla.TLAWordDetector;



public class PCalWordDetector extends TLAWordDetector implements IWordDetector {



	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.editor.basic.tla.TLAWordDetector#isWordPart(char)

	 */

	@Override

	public boolean isWordPart(final char character) {

		if (character == ':' || character == '=') {

			// Detect assignment ":=" as word.

			return true;

		} else if (character == '|') {

			// Detect multi-assignment "||" as word.

			return true;

		}

		return super.isWordPart(character);

	}

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/PCALCodeScanner.java

+1 −1
Original line number Diff line number Diff line
@@ -37,7 +37,7 @@ public class PCALCodeScanner extends RuleBasedScanner 
        IToken other = new Token(new TextAttribute(provider.getColor(TLAColorProvider.TLA_DEFAULT)));

        IToken pcal = new Token(new TextAttribute(provider.getColor(TLAColorProvider.PCAL_KEYWORD)));

        

        List rules = new ArrayList();

        List<WordRule> rules = new ArrayList<WordRule>();



        // Add generic whitespace rule.

        // rules.add(new WhitespaceRule(DocumentHelper.getDefaultWhitespaceDetector()));

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TLACompletionProcessor.java

+36 −147
Original line number Diff line number Diff line 
package org.lamport.tla.toolbox.editor.basic.tla;



import java.util.ArrayList;

import java.util.Arrays;

import java.util.List;



import org.eclipse.jface.text.BadLocationException;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IRegion;

import org.eclipse.jface.text.ITextViewer;

import org.eclipse.jface.text.contentassist.CompletionProposal;

import org.eclipse.jface.text.contentassist.ContextInformation;

import org.eclipse.jface.text.contentassist.ICompletionProposal;

import org.eclipse.jface.text.contentassist.IContentAssistProcessor;

import org.eclipse.jface.text.contentassist.IContextInformation;

import org.eclipse.jface.text.contentassist.IContextInformationValidator;

import org.eclipse.swt.graphics.Point;

import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;

import org.lamport.tla.toolbox.editor.basic.ToolboxCompletionProcessor;

import org.lamport.tla.toolbox.editor.basic.pcal.IPCalReservedWords;



/**

 * Syntactic auto-completion processor

 * @author Simon Zambrovski

 * @version $Id$

 */

public class TLACompletionProcessor implements IContentAssistProcessor

public class TLACompletionProcessor extends ToolboxCompletionProcessor implements IContentAssistProcessor

{

    private String[] proposals = ITLAReserveredWords.ALL_WORDS_ARRAY;



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#computeCompletionProposals(org.eclipse.jface.text.ITextViewer, int)

     */

    public ICompletionProposal[] computeCompletionProposals(ITextViewer viewer, int offset)

    {

        /*

        // show all proposals without checking the context

        ICompletionProposal[] result = new ICompletionProposal[fgProposals.length];

        for (int i = 0; i < fgProposals.length; i++)

        {

            IContextInformation info = new ContextInformation(fgProposals[i], "");

            result[i] = new CompletionProposal(fgProposals[i], offset, 0, fgProposals[i].length(), null,

                    fgProposals[i], info, "");

        }

        return result;

        */



        IDocument document = viewer.getDocument();

        // get the selection range

        Point selectedRange = viewer.getSelectedRange();



        List propList = new ArrayList();

        try

        {

            if (selectedRange.y > 0)

            {

                // the range is non-empty

                String text = document.get(selectedRange.x, selectedRange.y);

                computeWordProposals(text, offset, propList);

            } else

            {

                // the range is empty, no selection in the editor



                // get the region

                IRegion wordRegion = DocumentHelper.getRegionExpandedBackwards(document, offset, DocumentHelper

                        .getDefaultWordDetector());

                String word = document.get(wordRegion.getOffset(), wordRegion.getLength());

                TLAEditorActivator.getDefault().logDebug("Content assist for '" + word + "'" + wordRegion );

                computeWordProposals(word, offset, propList);

            }

        } catch (BadLocationException e)

        {

            // TODO Auto-generated catch block

            e.printStackTrace();

        }



        ICompletionProposal[] proposals = new ICompletionProposal[propList.size()];

        propList.toArray(proposals);



        return proposals;



    }



    /**

     * Syntax-based proposal based for word beginning

     * @param word

     * @param offset

     * @param propositionList

     */

    private void computeWordProposals(String word, int offset, List propositionList)

    {

        int qualifierLength = word.length();



        // Loop through all proposals

        for (int i = 0; i < proposals.length; i++)

        {

            String proposalText = proposals[i];



            // Check if proposal matches qualifier

            if (proposalText.startsWith(word))

            {

                // compute whole proposal text

                String text = proposalText + " ";



                // Derive cursor position

                int cursor = proposalText.length();



                // Construct proposal

                CompletionProposal proposal = new CompletionProposal(text, offset - qualifierLength, qualifierLength,

                        cursor);



                // and add to result list

                propositionList.add(proposal);

            }

    public TLACompletionProcessor() {

    	final List<String> asList = Arrays.asList(ITLAReserveredWords.ALL_WORDS_ARRAY);

    	for (String string : asList) {

    		final List<CompletionProposalTemplate> proposal = new ArrayList<CompletionProposalTemplate>(1);

    		proposal.add(new CompletionProposalTemplate(string + " "));

			proposals.put(string, proposal);

		}

    	

		// Define PCal "algorithm" here because the PCalCompletionProcessor is only

		// active inside an algorithm definition (chicken or egg problem).

		final List<CompletionProposalTemplate> l = new ArrayList<CompletionProposalTemplate>(1);

		l.add(new CompletionProposalTemplate(

				"(***************************************************************************\r\n"

						+ "--algorithm AlgorithmName {\r\n}\r\n"

						+ " ***************************************************************************)\r\n",

				IPCalReservedWords.ALGORITHM, IPCalReservedWords.ALGORITHM_HELP));

		proposals.put(ITLAReserveredWords.ALGORITHM, l);

    }



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#computeContextInformation(org.eclipse.jface.text.ITextViewer, int)

     */

    public IContextInformation[] computeContextInformation(ITextViewer viewer, int offset)

    {

	public IContextInformation[] computeContextInformation(ITextViewer viewer, int offset) {

		// Retrieve selected range

        Point selectedRange = viewer.getSelectedRange();

        if (selectedRange.y > 0)

        {

		final Point selectedRange = viewer.getSelectedRange();

		if (selectedRange.y > 0) {

			// Text is selected. Create a context information array.

            ContextInformation[] contextInfos = new ContextInformation[ITLAReserveredWords.ALL_WORDS_ARRAY.length];

			final IContextInformation[] contextInfos = new ContextInformation[ITLAReserveredWords.ALL_WORDS_ARRAY.length];



			// Create one context information item for each style

            for (int i = 0; i < ITLAReserveredWords.ALL_WORDS_ARRAY.length; i++)

			for (int i = 0; i < ITLAReserveredWords.ALL_WORDS_ARRAY.length; i++) {

				contextInfos[i] = new ContextInformation(null, ITLAReserveredWords.ALL_WORDS_ARRAY[i] + " Style");

			}

			return contextInfos;

		}

		return new ContextInformation[0];

	}



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getCompletionProposalAutoActivationCharacters()

     */

    public char[] getCompletionProposalAutoActivationCharacters()

    {

        return null;

    }



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getContextInformationAutoActivationCharacters()

     */

    public char[] getContextInformationAutoActivationCharacters()

    {

        return null;

    }



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getContextInformationValidator()

     */

    public IContextInformationValidator getContextInformationValidator()

    {

        return null;

    }



    /* (non-Javadoc)

     * @see org.eclipse.jface.text.contentassist.IContentAssistProcessor#getErrorMessage()

     */

    public String getErrorMessage()

    {

        return null;

    }



}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TLAHyperlinkDetector.java

+47 −34
Original line number Diff line number Diff line 
package org.lamport.tla.toolbox.editor.basic.tla;



import java.io.File;



import org.eclipse.core.filesystem.EFS;

import org.eclipse.core.filesystem.IFileStore;

import org.eclipse.core.resources.IFile;

import org.eclipse.core.resources.IResource;

import org.eclipse.core.runtime.CoreException;

import org.eclipse.core.runtime.Path;

import org.eclipse.jface.text.BadLocationException;

import org.eclipse.jface.text.IDocument;

import org.eclipse.jface.text.IRegion;
@@ -10,29 +14,26 @@ import org.eclipse.jface.text.ITextViewer; 
import org.eclipse.jface.text.Region;

import org.eclipse.jface.text.hyperlink.AbstractHyperlinkDetector;

import org.eclipse.jface.text.hyperlink.IHyperlink;

import org.eclipse.ui.IEditorInput;

import org.eclipse.ui.editors.text.FileDocumentProvider;

import org.eclipse.ui.editors.text.TextFileDocumentProvider;

import org.eclipse.ui.ide.FileStoreEditorInput;

import org.eclipse.ui.part.FileEditorInput;

import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.eclipse.ui.texteditor.IDocumentProvider;

import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;

import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;

import org.lamport.tla.toolbox.editor.basic.TLAEditorReadOnly;

import org.lamport.tla.toolbox.editor.basic.actions.OpenDeclarationAction;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper;

import org.lamport.tla.toolbox.editor.basic.util.EditorUtil;

import org.lamport.tla.toolbox.editor.basic.util.EditorUtil.StringAndLocation;

import org.lamport.tla.toolbox.tool.ToolboxHandle;

import org.lamport.tla.toolbox.ui.handler.OpenModuleHandler;

import org.lamport.tla.toolbox.util.ResourceHelper;



import tla2sany.modanalyzer.SpecObj;

import tla2sany.parser.SyntaxTreeNode;

import tla2sany.parser.TLAplusParserConstants;

import tla2sany.semantic.Context;

import tla2sany.semantic.ModuleNode;

import tla2sany.semantic.OpDefNode;

import tla2sany.semantic.SymbolNode;

import tla2sany.semantic.ThmOrAssumpDefNode;

import tla2sany.st.Location;

import tla2sany.st.SyntaxTreeConstants;

import util.UniqueString;

import util.FilenameToStream;



/**

 * Detects hyperlinks in TLA+ code
@@ -50,10 +51,6 @@ import util.UniqueString; 
public class TLAHyperlinkDetector extends AbstractHyperlinkDetector

{



    public TLAHyperlinkDetector()

    {

    }



    /**

     * This method first sets label to the token at the position indicated by the

     * region.  If the module is parsed and unmodified, it uses EditorUtil.getTokenAt
@@ -101,6 +98,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
            return null;

        }

        



        // Set region to the Region of the document described by currentTokenSpec

        // (this ugly re-use of a parameter name is kept from Simon's original

        // code), set label to the found symbol name, and set resolvedSymbol to
@@ -141,25 +139,40 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
                	TLAEditorActivator.getDefault().logDebug(csNode.getAttachedComments()[i]);

                }



                IResource resource = null;

				IDocumentProvider documentProvider = null;

				IEditorInput editorInput = null;

				String editorId = "";

				//

                if (ToolboxHandle.isUserModule(ResourceHelper.getModuleFileName(csNode.getFilename())))

                {

                    // resource

                    resource = ResourceHelper.getResourceByModuleName(csNode.getFilename());

                } else

                {

                    // TLAEditorActivator.getDefault().logDebug("A StandardModule '" + csNode.getFilename() + "' is requested...");

				final FilenameToStream resolver = ToolboxHandle.getSpecObj().getResolver();

				if (ToolboxHandle.isUserModule(ResourceHelper.getModuleFileName(csNode.getFilename()))) {

					editorId = TLAEditorAndPDFViewer.ID;

					editorInput = new FileEditorInput(

							(IFile) ResourceHelper.getResourceByModuleName(csNode.getFilename()));

					documentProvider = new FileDocumentProvider();

				} else if (resolver.isStandardModule(csNode.getFilename())) {

					// No point editing standard modules.

					editorId = TLAEditorReadOnly.ID;



					// Resolve the file via the FilenameToStream resolver in case a user has

					// provided its own standard module definition.

					final File resolved = resolver.resolve(csNode.getFilename(), true);



					// Standard modules live outside the workspace which is why they have to be

					// opened with EFS and read with a TextFileDocumentProvider.

					final IFileStore fileStore = EFS.getLocalFileSystem()

							.getStore(new Path(resolved.getAbsolutePath()));

					editorInput = new FileStoreEditorInput(fileStore);

					documentProvider = new TextFileDocumentProvider();

				} else {

					// A TLA+ built-in module.

					return null;

				}



                // connect to the resource

                FileEditorInput fileEditorInput = new FileEditorInput((IFile) resource);

                FileDocumentProvider fileDocumentProvider = new FileDocumentProvider();

                try

                {

                    fileDocumentProvider.connect(fileEditorInput);

                    document = fileDocumentProvider.getDocument(fileEditorInput);

                    documentProvider.connect(editorInput);

                    document = documentProvider.getDocument(editorInput);

                } finally

                {

                    /*
@@ -169,7 +182,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
                     * Keeping it connected only seems to provide synchronization of

                     * the document with file changes. That is not necessary in this context.

                     */

                    fileDocumentProvider.disconnect(fileEditorInput);

                    documentProvider.disconnect(editorInput);

                }



                try
@@ -178,7 +191,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
                    // to get just the symbol from the left-hand side. (Otherwise,

                    // the user can't execute Goto Declaration immediately followed

                    // by Show Uses.)

                    if (resolvedSymbol instanceof OpDefNode)

                    if (resolvedSymbol instanceof OpDefNode && csNode.getHeirs().length >= 1)

                    {

                        // Need to pick out the symbol from the left-hand side of

                        // the definition.
@@ -194,7 +207,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
                                csNode = csNode.getHeirs()[1];

                            }

                        }

                    } else if ((resolvedSymbol instanceof ThmOrAssumpDefNode)

                    } else if ((resolvedSymbol instanceof ThmOrAssumpDefNode && csNode.getHeirs().length >= 2)

                            && ((csNode.getKind() == SyntaxTreeConstants.N_Theorem) || (csNode.getKind() == SyntaxTreeConstants.N_Assumption)))

                    {

                        csNode = csNode.getHeirs()[1];
@@ -206,7 +219,7 @@ public class TLAHyperlinkDetector extends AbstractHyperlinkDetector 
                    int startOffset = startLineRegion.getOffset() + csNode.getLocation().beginColumn() - 1;

                    int endOffset = endLineRegion.getOffset() + csNode.getLocation().endColumn();



                    return new IHyperlink[] { new OpenDeclarationAction(resource, new Region(startOffset, endOffset

                    return new IHyperlink[] { new OpenDeclarationAction(editorId, editorInput, new Region(startOffset, endOffset

                            - startOffset), label, region) };



                } catch (BadLocationException e)

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/tla/TokenSpec.java

+8 −2
Original line number Diff line number Diff line
@@ -148,9 +148,15 @@ public class TokenSpec 
            int rightPos = tokenSpecs[i].rightPos;

            tokenSpecs[i].leftPos = leftPos + offsetOfLine;

            tokenSpecs[i].rightPos = rightPos + offsetOfLine;



            String indiceAdjustedToken = tokenSpecs[i].token;

            Location location = EditorUtil.getLocationAt(document, tokenSpecs[i].leftPos, rightPos - leftPos);

            symbol = EditorUtil.lookupOriginalSymbol(UniqueString.uniqueStringOf(tokenSpecs[i].token), moduleNode,

                    location, null);

            

            if ((indiceAdjustedToken != null) && (indiceAdjustedToken.length() > 1) && (indiceAdjustedToken.charAt(0) == '_')) {

                indiceAdjustedToken = indiceAdjustedToken.substring(1);

            }

            

            symbol = EditorUtil.lookupOriginalSymbol(UniqueString.uniqueStringOf(indiceAdjustedToken), moduleNode, location, null);

            if (symbol != null)

            {

                goodIndex = i;

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/util/DocumentHelper.java

+29 −7
Original line number Diff line number Diff line
@@ -15,7 +15,6 @@ import tla2sany.st.Location; 
/**

 * Toolkit for document helper methods

 * @author Simon Zambrovski

 * @version $Id$

 */

public class DocumentHelper

{
@@ -110,18 +109,28 @@ public class DocumentHelper 
        return new Region(documentOffset - charCounter, charCounter + 1);

    }

    

    /**

     * @see DocumentHelper#getRegionExpandedBoth(IDocument, int, IWordDetector)

     */

    public static WordRegion getRegionExpandedBoth(IDocument document, int documentOffset) throws BadLocationException

    {

    	return getRegionExpandedBoth(document, documentOffset, getDefaultWordDetector());

    }



    /**

     * Combines the effect of backwards and forwards region expansion

     * @param document

     * @param offset

     * @param defaultWordDetector

     * @return

     * @return A {@link WordRegion} or null if no region could be found.

     * @throws BadLocationException 

     */

    public static IRegion getRegionExpandedBoth(IDocument document, int documentOffset, IWordDetector detector)

    public static WordRegion getRegionExpandedBoth(IDocument document, int documentOffset, IWordDetector detector) throws BadLocationException

    {

        IRegion backwards = getRegionExpandedBackwards(document, documentOffset, detector);

        IRegion forwards = getRegionExpandedForwards(document, documentOffset, detector);

        return new Region(backwards.getOffset(), backwards.getLength() + forwards.getLength());

        final IRegion backwards = getRegionExpandedBackwards(document, documentOffset, detector);

        final IRegion forwards = getRegionExpandedForwards(document, documentOffset, detector);

        final String word = document.get(backwards.getOffset(), backwards.getLength() + forwards.getLength());

        return new WordRegion(backwards.getOffset(), backwards.getLength() + forwards.getLength(), word);

    }



    /**
@@ -187,6 +196,19 @@ public class DocumentHelper 
            // no previous line so do nothing

            return region;

        }

    }

    

    public static class WordRegion extends Region implements IRegion {



		private final String word;



		public WordRegion(int offset, int length, String word) {

			super(offset, length);

			this.word = word;

		}

		

		public String getWord() {

			return word;

		}

    }

}

org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/util/EditorUtil.java

+20 −0
Original line number Diff line number Diff line
@@ -21,6 +21,7 @@ import org.lamport.tla.toolbox.Activator; 
import org.lamport.tla.toolbox.editor.basic.TLAEditor;

import org.lamport.tla.toolbox.editor.basic.TLAEditorActivator;

import org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer;

import org.lamport.tla.toolbox.editor.basic.util.DocumentHelper.WordRegion;

import org.lamport.tla.toolbox.spec.Spec;

import org.lamport.tla.toolbox.spec.parser.IParseConstants;

import org.lamport.tla.toolbox.spec.parser.ParseResult;
@@ -30,6 +31,7 @@ import org.lamport.tla.toolbox.util.ResourceHelper; 
import org.lamport.tla.toolbox.util.UIHelper;



import pcal.TLAtoPCalMapping;

import tla2sany.modanalyzer.SpecObj;

import tla2sany.parser.Operators;

import tla2sany.parser.SyntaxTreeNode;

import tla2sany.semantic.AssumeProveNode;
@@ -447,6 +449,24 @@ public class EditorUtil 
        return loc;

    }

    

    /**

     * @see EditorUtil#lookupSymbol(UniqueString, SemanticNode, Location, SymbolNode)

     */

 	public static SymbolNode lookupSymbol(SpecObj specObj, IDocument document, WordRegion region) {

		final Location location = getLocationAt(document, region.getOffset(), region.getLength());

		final ModuleNode rootModule = specObj.getExternalModuleTable().getRootModule();

		return lookupSymbol(UniqueString.uniqueStringOf(region.getWord()), rootModule, location, null);

	}

    

 	/**

 	 * @see EditorUtil#lookupSymbol(UniqueString, SemanticNode, Location, SymbolNode)

 	 */

	public static SymbolNode lookupSymbol(String name, SymbolNode curNode, IDocument document, IRegion region,

			SymbolNode defaultResult) {

		final Location location = getLocationAt(document, region.getOffset(), region.getLength());

		return lookupSymbol(UniqueString.uniqueStringOf(name), curNode, location, defaultResult);

	}



    /**

     * This method is called externally with <code>curNode</code> equal to

     * a ModuleNode and <code>defaultResult</code> equal to <code>null</code>.

org.lamport.tla.toolbox.feature.branding/feature.xml

+21 −71
Original line number Diff line number Diff line
@@ -5,78 +5,28 @@ 
      version="1.0.0.qualifier"

      provider-name="Leslie Lamport, Markus Alexander Kuppe">



   <description url="http://www.example.com/description">

      [Enter Feature Description here.]

   </description>



   <copyright>

      This feature contains branding¹ information like the License Agreement.



¹ &quot;branding&quot; is an Eclipse specific term.

   </copyright>



   <license url="">

      Unless otherwise indicated, the TLA Toolbox is made available by Microsoft Corporation under the terms and conditions of the Microsoft Research License Agreement provided below.  The Compaq Corporation license below governs some of the code located in subdirectories tla2sany, tla2tex, tlc2, and util of the file tla2tools.jar.  

  

IT IS YOUR OBLIGATION TO READ AND ACCEPT ALL SUCH TERMS AND CONDITIONS PRIOR TO USE

Microsoft Research License Agreement

TLA Toolbox



This Microsoft Research License Agreement (&quot;MSR-LA&quot;) is a legal agreement between you and Microsoft Corporation (“Microsoft” or “we”) for the software or data identified above, which may include source code, and any associated materials, text or speech files, associated media and &quot;online&quot; or electronic documentation and any updates we provide in our discretion (together, the &quot;Software&quot;). 



By installing, copying, or otherwise using this Software, found at http://research.microsoft.com/downloads, you agree to be bound by the terms of this MSR-LA.  If you do not agree, do not install copy or use the Software. The Software is protected by copyright and other intellectual property laws and is licensed, not sold.    

SCOPE OF RIGHTS:

You may use, copy, reproduce, and distribute this Software for any non-commercial purpose, subject to the restrictions in this MSR-LA. Some purposes which can be non-commercial are teaching, academic research, public demonstrations and personal experimentation. You may also distribute this Software with books or other teaching materials, or publish the Software on websites, that are intended to teach the use of the Software for academic or other non-commercial purposes.

You may not use or distribute this Software or any derivative works in any form for commercial purposes. Examples of commercial purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial products, or any other activity which purpose is to procure a commercial gain to you or others.  Notwithstanding the foregoing, if you are a commercial entity, you may use this software solely for your own internal use.

If the Software includes source code or data, you may create derivative works of such portions of the Software and distribute the modified Software for non-commercial purposes, as provided herein.  

If you distribute the Software or any derivative works of the Software, you will distribute them under the same terms and conditions as in this license, and you will not grant other rights to the Software or derivative works that are different from those provided by this MSR-LA. 

If you have created derivative works of the Software, and distribute such derivative works, you will cause the modified files to carry prominent notices so that recipients know that they are not receiving the original Software. Such notices must state: (i) that you have changed the Software; and (ii) the date of any changes.

In return, we simply require that you agree: 

1. That you will not remove any copyright or other notices from the Software.

2. That if any of the Software is in binary format, you will not attempt to modify such portions of the Software, or to reverse engineer or decompile them, except and only to the extent authorized by applicable law. 

3. That you will not use the Software in a live operating environment where it may be relied upon to perform in the same manner as a commercially released product, or with data that has not been sufficiently backed up.

4. That Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose.  

5. That any feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential. 

6. THAT THE SOFTWARE COMES &quot;AS IS&quot;, WITH NO WARRANTIES. THIS MEANS NO EXPRESS, IMPLIED OR STATUTORY WARRANTY, INCLUDING WITHOUT LIMITATION, WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE, ANY WARRANTY AGAINST INTERFERENCE WITH YOUR ENJOYMENT OF THE SOFTWARE OR ANY WARRANTY OF TITLE OR NON-INFRINGEMENT. THERE IS NO WARRANTY THAT THIS SOFTWARE WILL FULFILL ANY OF YOUR PARTICULAR PURPOSES OR NEEDS. ALSO, YOU MUST PASS THIS DISCLAIMER ON WHENEVER YOU DISTRIBUTE THE SOFTWARE OR DERIVATIVE WORKS.

7. THAT NEITHER MICROSOFT NOR ANY CONTRIBUTOR TO THE SOFTWARE WILL BE LIABLE FOR ANY DAMAGES RELATED TO THE SOFTWARE OR THIS MSR-LA, INCLUDING DIRECT, INDIRECT, SPECIAL, CONSEQUENTIAL OR INCIDENTAL DAMAGES, TO THE MAXIMUM EXTENT THE LAW PERMITS, NO MATTER WHAT LEGAL THEORY IT IS BASED ON. ALSO, YOU MUST PASS THIS LIMITATION OF LIABILITY ON WHENEVER YOU DISTRIBUTE THE SOFTWARE OR DERIVATIVE WORKS.

8. That we have no duty of reasonable care or lack of negligence, and we are not obligated to (and will not) provide technical support for the Software.

9. That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone&apos;s use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically.  Upon any such termination, you shall destroy all of your copies of the Software immediately.  Sections 4, 5, 6, 7, 8, 9, 12 and 13 of this MSR-LA shall survive any termination of this MSR-LA.

10. That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make.

11. That the Software may be subject to U.S. export jurisdiction at the time it is licensed to you, and it may be subject to additional export or import laws in other places.  You agree to comply with all such laws and regulations that may apply to the Software after delivery of the software to you.

12. That all rights not expressly granted to you in this MSR-LA are reserved.

13. That this MSR-LA shall be construed and controlled by the laws of the State of Washington, USA, without regard to conflicts of law.  If any provision of this MSR-LA shall be deemed unenforceable or contrary to law, the rest of this MSR-LA shall remain in full effect and interpreted in an enforceable manner that most nearly captures the intent of the original language. 



The following license applies to code marked with the following notice:

Copyright (c) 2003  

Compaq Corporation.  All rights reserved.



Compaq Computer Corporation, a Delaware corporation with offices at

20555 SH 249, Houston, TX, (COMPAQ) and you the CUSTOMER agree as

follows:



Permission is hereby granted, free of charge, to any person obtaining

a copy of this software and associated documentation files (the

&quot;Software&quot;), 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 &quot;AS IS&quot;, 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 COMPAQ 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.



Except as contained in this notice, the name of COMPAQ shall not be

used in advertising or otherwise to promote the sale, use or other

dealings in this Software without prior written authorization from

COMPAQ.

      MIT License



Copyright (c) 2018 Microsoft Corporation



Permission is hereby granted, free of charge, to any person obtaining a copy

of this software and associated documentation files (the &quot;Software&quot;), 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 &quot;AS IS&quot;, 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.

   </license>



</feature>

org.lamport.tla.toolbox.jclouds/META-INF/MANIFEST.MF

+1 −1
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ Require-Bundle: org.eclipse.core.runtime, 
 jclouds-scriptbuilder;bundle-version="1.7.3",

 jclouds-slf4j;bundle-version="1.7.3",

 jclouds-sshj;bundle-version="1.7.3",

 com.google.guava;bundle-version="15.0.0",

 com.google.guava;bundle-version="[15.0.0,21.0.0)",

 com.google.inject;bundle-version="3.0.0",

 org.apache.commons.io;bundle-version="2.0.1",

 org.lamport.tlatools;bundle-version="1.0.0"

org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/AzureCloudTLCInstanceParameters.java

+4 −63
Original line number Diff line number Diff line
@@ -89,7 +89,7 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters 
	public String getImageId() {

		// 'azure vm image list eastus canonical' (manually lookup image release date from output)

		// With azure-cli v2 (based on Python) extract date from 'az vm image list --all --publisher Canonical'.

		return System.getProperty("azure.image", "b39f27a8b8c64d52b05eac6a62ebad85__Ubuntu-16_04-LTS-amd64-server-20180112-en-us-30GB");

		return System.getProperty("azure.image", "b39f27a8b8c64d52b05eac6a62ebad85__Ubuntu-18_04-LTS-amd64-server-20180426.2-en-us-30GB");

	}



	/* (non-Javadoc)
@@ -140,7 +140,9 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters 
					"Invalid credentials, please check the environment variables "

							+ "(AZURE_COMPUTE_CREDENTIALS & AZURE_COMPUTE_IDENTITY "

							+ "and AZURE_COMPUTE_SUBSCRIPTION) are correctly "

							+ "set up and picked up by the Toolbox.");

							+ "set up and picked up by the Toolbox."

							+ "\n\nPlease visit the Toolbox help and read section 4 "

							+ "of \"Cloud based distributed TLC\" on how to setup authentication.");

		}

		// Verify that the identity file exists.

		final File file = new File(identity);
@@ -159,24 +161,6 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters 
		builder.endpoint("https://management.core.windows.net/" + getSubscriptionId());

	}

	

	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getExtraRepositories()

	 */

	@Override

	public String getExtraRepositories() {

		return "echo \"deb [arch=amd64] https://packages.microsoft.com/repos/azure-cli/ wheezy main\" | sudo tee /etc/apt/sources.list.d/azure-cli.list && apt-key adv --keyserver packages.microsoft.com --recv-keys 417A0893";

	}



	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getExtraPackages()

	 */

	@Override

	public String getExtraPackages() {

		// https://docs.microsoft.com/en-us/cli/azure/install-azure-cli?view=azure-cli-latest#install-on-debianubuntu-with-apt-get

		// see getExtraRepositories too.

		return "azure-cli";

	}

	

	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getHostnameSetup()

	 */
@@ -192,47 +176,4 @@ public class AzureCloudTLCInstanceParameters extends CloudTLCInstanceParameters 
		// (similar to EC2CloudTLCInstanceParameters#getHostnameSetup.

		return "hostname \"$(hostname).cloudapp.net\" && echo \"$(curl -s ifconfig.co) $(hostname)\" >> /etc/hosts";

	}



	/* (non-Javadoc)

	 * @see org.lamport.tla.toolbox.jcloud.CloudTLCInstanceParameters#getCleanup()

	 */

	@Override

	public String getCloudAPIShutdown() {

		final String servicePrincipal = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL");

		final String password = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_PASSWORD");

		final String tenant = System.getenv("AZURE_COMPUTE_SERVICE_PRINCIPAL_TENANT");

		if (servicePrincipal == null || password == null || tenant == null) {

			// Missing credentials.

			return super.getCloudAPIShutdown();

		}

		// What we try to accomplish is to purge the complete Azure Resource Group (a RG

		// combines all Azure resources associated with the VM (storage, networking,

		// ips, ...).

		// The way we do it, is to use the azure CLI to deploy the template in

		// /tmp/rg.json created by the printf statement under the same resource group

		// identify we wish to purge. The trick is, that the template defines no

		// resources whatsoever. This effectively purges the old resources in the

		// resource group. Idea taken from

		// http://www.codeisahighway.com/effective-ways-to-delete-resources-in-a-resource-group-on-azure/

		// bash/screen/ssh apparently fiddle with quotes and which is why the json is base64 encoded 

		// and decoded on the instance:

		// { "$schema": "https://schema.management.azure.com/schemas/2015-01-01/deploymentTemplate.json#", "contentVersion": "1.0.0.0", "parameters": {}, "variables": {}, "resources": [], "outputs": {} } | base64

		//

		// Unfortunately, the azure CLI needs credentials to talk to the Azure API. For

		// that, one manually creates a service principal once as described in

		// https://docs.microsoft.com/en-us/cli/azure/create-an-azure-service-principal-azure-cli?view=azure-cli-latest

		// and uses it to log into Azure as described in

		// https://docs.microsoft.com/en-us/cli/azure/authenticate-azure-cli?view=azure-cli-latest.

		// Using AZURE_COMPUTE_CREDENTIALS and AZURE_COMPUTE_IDENTITY to login with azure CLI

		// would trigger a two-factor auth for Microsoft FTEs. Not something we want.

		//

		// An alternative might be to use an auth.properties file, but this doesn't seem

		// supported by azure CLI yet. Read "File based authentication" at

		// https://docs.microsoft.com/en-us/java/azure/java-sdk-azure-authenticate#mgmt-file

		return "echo eyAiJHNjaGVtYSI6ICJodHRwczovL3NjaGVtYS5tYW5hZ2VtZW50LmF6dXJlLmNvbS9zY2hlbWFzLzIwMTUtMDEtMDEvZGVwbG95bWVudFRlbXBsYXRlLmpzb24jIiwgImNvbnRlbnRWZXJzaW9uIjogIjEuMC4wLjAiLCAicGFyYW1ldGVycyI6IHt9LCAidmFyaWFibGVzIjoge30sICJyZXNvdXJjZXMiOiBbXSwgIm91dHB1dHMiOiB7fSB9Cg== | base64 -d > /tmp/rg.json"

				+ " && " + "az login --service-principal -u \"" + servicePrincipal + "\" -p " + password + " --tenant "

				// $(hostname -s) only works iff hostname is correctly setup with getHostnameSetup() above.

				+ tenant + " && " + "az group deployment create --resource-group $(hostname -s)"

				+ " --template-file /tmp/rg.json --mode Complete";

	}

}

org.lamport.tla.toolbox.product.product/pom.xml

+1 −1
Original line number Diff line number Diff line
@@ -19,7 +19,7 @@ 
    <!-- Align product.version with the version in 

         org.lamport.tla.toolbox.product.product.product

         product.version. -->

    <product.version>1.5.6</product.version>

    <product.version>1.5.7</product.version>

    <!-- Format build timestamp to adhere to the Debian package guidelines -->

    <maven.build.timestamp.format>yyyyMMdd-HHmm</maven.build.timestamp.format>

    <product.build>${maven.build.timestamp}</product.build>

pom.xml

+1 −11

File changed.

Preview size limit exceeded, changes collapsed.

tlatools/.classpath

+2 −0

File changed.

Preview size limit exceeded, changes collapsed.

tlatools/build.gradle

+2 −2

File changed.

Preview size limit exceeded, changes collapsed.

tlatools/pom.xml

+2 −2

File changed.

Preview size limit exceeded, changes collapsed.