TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
Home Page: https://lamport.azurewebsites.net/tla/tla.html
License: MIT License
For more information, visit http://lamport.azurewebsites.net/tla/tla.html
Please read our contribution guide before you start working on your contribution. We also have a feature wishlist.
Copyright (c) 199?-2003 HP Corporation
Copyright (c) 2003-2020 Microsoft Corporation
Licensed under the MIT License
![azure-pipelines[bot] avatar](https://avatars.githubusercontent.com/in/9426?v=4 "azure-pipelines[bot]")
TLC (TLC2 Version 2.08 of 21 December 2015) throws an incomplete error message when the operator TLCSet of the standard module TLC is used within the INIT predicate:
Attempted to apply the operator overridden by the Java method
public static tlc2.value.Value tlc2.module.TLC.TLCSet(tlc2.value.Value,tlc2.value.Value),
but it produced the following error:
%2%
The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty.
for module:
----- MODULE ModuleTLC -----
EXTENDS Integers, TLC
VARIABLES x
Init == x = 1 /\ TLCSet(1,"TLCSet works.")
Next == x < 10 /\ x' = x + 1 /\ PrintT(TLCGet(1))
=====
ModuleTLC.zip
Using an older version of TLC (TLC2 Version 2.06 of 9 May 2015) the TLCSet operator works properly within the INIT predicate.
When trying to open the model editor, I get the following:
Plug-in "org.lamport.tla.toolbox.tool.tlc.ui" was unable to instantiate class "org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor".
Version 1.5.3
System information:
$ java -version
openjdk version "9-internal"
OpenJDK Runtime Environment (build 9-internal+0-2016-04-14-195246.buildd.src)
OpenJDK 64-Bit Server VM (build 9-internal+0-2016-04-14-195246.buildd.src, mixed mode)
$ uname -a
Linux apghero 4.4.0-72-generic #93-Ubuntu SMP Fri Mar 31 14:07:41 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
$ cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=16.04
DISTRIB_CODENAME=xenial
DISTRIB_DESCRIPTION="Ubuntu 16.04.2 LTS"StackTrace:
org.eclipse.core.runtime.CoreException: Plug-in "org.lamport.tla.toolbox.tool.tlc.ui" was unable to instantiate class "org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor".
at org.eclipse.core.internal.registry.osgi.RegistryStrategyOSGI.throwException(RegistryStrategyOSGI.java:194)
at org.eclipse.core.internal.registry.osgi.RegistryStrategyOSGI.createExecutableExtension(RegistryStrategyOSGI.java:186)
at org.eclipse.core.internal.registry.ExtensionRegistry.createExecutableExtension(ExtensionRegistry.java:905)
at org.eclipse.core.internal.registry.ConfigurationElement.createExecutableExtension(ConfigurationElement.java:243)
at org.eclipse.core.internal.registry.ConfigurationElementHandle.createExecutableExtension(ConfigurationElementHandle.java:55)
at org.eclipse.ui.internal.WorkbenchPlugin.createExtension(WorkbenchPlugin.java:285)
at org.eclipse.ui.internal.registry.EditorDescriptor.createEditor(EditorDescriptor.java:235)
at org.eclipse.ui.internal.EditorReference.createPart(EditorReference.java:328)
at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.createPart(CompatibilityPart.java:279)
at org.eclipse.ui.internal.e4.compatibility.CompatibilityEditor.createPart(CompatibilityEditor.java:63)
at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.create(CompatibilityPart.java:317)
at sun.reflect.NativeMethodAccessorImpl.invoke0(java.base@9-internal/Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(java.base@9-internal/NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(java.base@9-internal/DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(java.base@9-internal/Method.java:531)
at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56)
at org.eclipse.e4.core.internal.di.InjectorImpl.processAnnotated(InjectorImpl.java:898)
at org.eclipse.e4.core.internal.di.InjectorImpl.processAnnotated(InjectorImpl.java:879)
at org.eclipse.e4.core.internal.di.InjectorImpl.inject(InjectorImpl.java:121)
at org.eclipse.e4.core.internal.di.InjectorImpl.internalMake(InjectorImpl.java:345)
at org.eclipse.e4.core.internal.di.InjectorImpl.make(InjectorImpl.java:264)
at org.eclipse.e4.core.contexts.ContextInjectionFactory.make(ContextInjectionFactory.java:162)
at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.createFromBundle(ReflectionContributionFactory.java:104)
at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.doCreate(ReflectionContributionFactory.java:73)
at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.create(ReflectionContributionFactory.java:55)
at org.eclipse.e4.ui.workbench.renderers.swt.ContributedPartRenderer.createWidget(ContributedPartRenderer.java:129)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.createWidget(PartRenderingEngine.java:971)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.safeCreateGui(PartRenderingEngine.java:640)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.safeCreateGui(PartRenderingEngine.java:746)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.access$0(PartRenderingEngine.java:717)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$2.run(PartRenderingEngine.java:711)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.createGui(PartRenderingEngine.java:695)
at org.eclipse.e4.ui.internal.workbench.PartServiceImpl$1.handleEvent(PartServiceImpl.java:99)
at org.eclipse.e4.ui.services.internal.events.UIEventHandler$1.run(UIEventHandler.java:40)
at org.eclipse.swt.widgets.Synchronizer.syncExec(Synchronizer.java:186)
at org.eclipse.ui.internal.UISynchronizer.syncExec(UISynchronizer.java:145)
at org.eclipse.swt.widgets.Display.syncExec(Display.java:4633)
at org.eclipse.e4.ui.internal.workbench.swt.E4Application$1.syncExec(E4Application.java:211)
at org.eclipse.e4.ui.services.internal.events.UIEventHandler.handleEvent(UIEventHandler.java:36)
at org.eclipse.equinox.internal.event.EventHandlerWrapper.handleEvent(EventHandlerWrapper.java:197)
at org.eclipse.equinox.internal.event.EventHandlerTracker.dispatchEvent(EventHandlerTracker.java:197)
at org.eclipse.equinox.internal.event.EventHandlerTracker.dispatchEvent(EventHandlerTracker.java:1)
at org.eclipse.osgi.framework.eventmgr.EventManager.dispatchEvent(EventManager.java:230)
at org.eclipse.osgi.framework.eventmgr.ListenerQueue.dispatchEventSynchronous(ListenerQueue.java:148)
at org.eclipse.equinox.internal.event.EventAdminImpl.dispatchEvent(EventAdminImpl.java:135)
at org.eclipse.equinox.internal.event.EventAdminImpl.sendEvent(EventAdminImpl.java:78)
at org.eclipse.equinox.internal.event.EventComponent.sendEvent(EventComponent.java:39)
at org.eclipse.e4.ui.services.internal.events.EventBroker.send(EventBroker.java:85)
at org.eclipse.e4.ui.internal.workbench.UIEventPublisher.notifyChanged(UIEventPublisher.java:59)
at org.eclipse.emf.common.notify.impl.BasicNotifierImpl.eNotify(BasicNotifierImpl.java:374)
at org.eclipse.e4.ui.model.application.ui.impl.ElementContainerImpl.setSelectedElement(ElementContainerImpl.java:171)
at org.eclipse.e4.ui.internal.workbench.ModelServiceImpl.showElementInWindow(ModelServiceImpl.java:572)
at org.eclipse.e4.ui.internal.workbench.ModelServiceImpl.bringToTop(ModelServiceImpl.java:536)
at org.eclipse.e4.ui.internal.workbench.PartServiceImpl.delegateBringToTop(PartServiceImpl.java:724)
at org.eclipse.e4.ui.internal.workbench.PartServiceImpl.showPart(PartServiceImpl.java:1163)
at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditor(WorkbenchPage.java:3252)
at org.eclipse.ui.internal.WorkbenchPage.access$25(WorkbenchPage.java:3167)
at org.eclipse.ui.internal.WorkbenchPage$10.run(WorkbenchPage.java:3149)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3144)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3108)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3089)
at org.lamport.tla.toolbox.util.UIHelper.openEditor(UIHelper.java:352)
at org.lamport.tla.toolbox.util.UIHelper.openEditor(UIHelper.java:337)
at org.lamport.tla.toolbox.tool.tlc.handlers.StartLaunchHandler.execute(StartLaunchHandler.java:48)
at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:295)
at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90)
at sun.reflect.NativeMethodAccessorImpl.invoke0(java.base@9-internal/Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(java.base@9-internal/NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(java.base@9-internal/DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(java.base@9-internal/Method.java:531)
at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56)
at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:252)
at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:234)
at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132)
at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:152)
at org.eclipse.core.commands.Command.executeWithChecks(Command.java:493)
at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:486)
at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210)
at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:799)
at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:675)
at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:659)
at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:592)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4481)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1329)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3819)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3430)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
at org.lamport.tla.toolbox.Application.start(Application.java:93)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
at sun.reflect.NativeMethodAccessorImpl.invoke0(java.base@9-internal/Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(java.base@9-internal/NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(java.base@9-internal/DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(java.base@9-internal/Method.java:531)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)
at org.eclipse.equinox.launcher.Main.run(Main.java:1515)
at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
Caused by: java.lang.reflect.InaccessibleObjectException: Unable to make member of class com.sun.management.internal.OperatingSystemImpl accessible: module jdk.management does not export com.sun.management.internal to unnamed module @5939f047
at sun.reflect.Reflection.throwInaccessibleObjectException(java.base@9-internal/Reflection.java:420)
at java.lang.reflect.AccessibleObject.checkCanSetAccessible(java.base@9-internal/AccessibleObject.java:174)
at java.lang.reflect.Method.checkCanSetAccessible(java.base@9-internal/Method.java:189)
at java.lang.reflect.Method.setAccessible(java.base@9-internal/Method.java:183)
at util.TLCRuntime.getPhysicalSystemMemory(TLCRuntime.java:50)
at util.TLCRuntime.getAbsolutePhysicalSystemMemory(TLCRuntime.java:69)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.MainModelPage.<init>(MainModelPage.java:200)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.<init>(ModelEditor.java:205)
at sun.reflect.NativeConstructorAccessorImpl.newInstance0(java.base@9-internal/Native Method)
at sun.reflect.NativeConstructorAccessorImpl.newInstance(java.base@9-internal/NativeConstructorAccessorImpl.java:62)
at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(java.base@9-internal/DelegatingConstructorAccessorImpl.java:45)
at java.lang.reflect.Constructor.newInstance(java.base@9-internal/Constructor.java:453)
at java.lang.Class.newInstance(java.base@9-internal/Class.java:550)
at org.eclipse.core.internal.registry.osgi.RegistryStrategyOSGI.createExecutableExtension(RegistryStrategyOSGI.java:184)
... 109 more
xxyzz: "When you open NewLinearSnapshot and then Model_2, you will find an error trace and the state function Dom selected in the Trace Explorer. (If not, run the model.) Running the trace explorer produces a blank TLC Errors window (which I have to ask the Toolbox to display), and the TLC Console shows that the TE file ran without an error, though it produced only 2 distinct states when the error trace has three states. It looks like the TE file should only produce two states, so my guess is that the bug is in the creation of the TE file, and indeed I get the same thing if I ask it to display a trivial state function. Running the model again recreates the error trace."
NodePtrTable does not overflow to secondary storage and thus always eventually goes OOM if the model is large enough. It also throws an OOM, when NodePtrTable's capacity approaches Integer.MAX_VALUE - the JVM's built-in limit for array. Subsequently an ArrayIndexOutOfBound exception gets thrown because NodePtrTable's length increases prior to the OOM and does not readjusted in case of an OOM.
NodePtrTable.grow() line: 132
NodePtrTable.get(long) line: 76
DiskGraph.getNode(long) line: 39
LiveCheck$LiveChecker.addNextState(TLCState, long, SetOfStates, BitVector, boolean[]) line: 454
LiveCheck.addNextState(TLCState, long, SetOfStates) line: 104
ModelChecker.doNext(TLCState, ObjLongTable, Worker) line: 619
Worker.run() line: 57
Howdy... I've very interested in using TLA+ and the code in this repository for a project I'm working on (https://funcatron.org). However, I'm unclear as to the license that governs the code. Some files seem to be MIT licensed. There's a license file (https://github.com/tlaplus/tlaplus/blob/master/tlatools/doc/License.txt) that is 14 years old. And there's a reference to the Microsoft Research License in some files.
Clarification of license terms would be greatly appreciated.
Thanks!!
xxyzzn:
A flag should be aded to modules which are built-in and are loaded by SANY from a specific folder. This information is required for the PM in order to overide the symbols. For example, the Integer.tla module should, if loaded from the pre-configured location, be labelled with "dummy=true" or "build-in=true" in the SANY syntax tree.
libal:
I just confirmed that the SANY parser reports the operators in Naturals, TLAPS and other library modules with kind UserDefinedOpKind. Since these operators have fixed semantics, it would be nice to have them under kind BuiltInKind.
xxyzzn:
The operators in Naturals, etc. are not built-in operators, so it would be very un-nice if SANY reported them as such. For example, it would make it impossible for the user to have TLC override the definition of the operator Seq from the Sequences module.
xxyzzn:
A field named isStandard that indicates if the module is a standard module was added to the ModuleNode class in the version of the code I just committed.
A prover bug causes tlapm to run forever checking the theorem in the enclosed file. It also ignores the command the Toolbox sends it when the user hits “cancel”. It’s necessary to kill tlapm from the OS, which naturally leaves the fingerprint file it’s writing in a bad state. I then added the theorem
THEOREM 22+33=44
BY Isa
which runs Isabelle until it times out. When I then run the prover on that theorem, it naturally raises this error/warning:
However, tlapm keeps running. Part of the Toolbox knows that tlapm is still running, because it displays
at the bottom. However, part of the Toolbox doesn’t know that tlapm is running because it does NOT raise this usual window:
I don’t know if this is a Toolbox bug, or if it’s caused by tlapm not interacting properly with the Toolbox. Of course, the user shouldn’t have to kill tlapm, so tlapm shouldn’t ever produce a bad fingerprint file. But, it would be nice if this didn’t happen when he did. So we should see if there’s a simple fix to this.
dougma:
There's a TLC preference called "Maximum JVM heap size..."
Seems it's the actual heap size, rather than the maximum. The description in overview-page.html also seems to suggest this.
Its default setting is 25%, which on my 8GB machine (when running the 32bit version) causes this error in the TLC console:
Error occurred during initialization of VM
Could not reserve enough space for 2058240KB object heap
I was further confused because this error only shows in the TLC console, and the "Model Checking Results" window doesn't indicate an error. This was my first attempt at running a model as i followed along in the hyperbook.
Reducing the setting to 10% and recreating my model I was able to continue.
The pragma information is contained in comments, which are not exported. There was a suggestion to use an operator PRAGMA and pass the pragma information as an argument. The pm will expect the same syntax as currently defined in the comments.
Todo:
Running TLC in depth-first mode with more than a single worker causes the TLC process to never terminate. A test case has been added with commit 9d1bee7. The method tlc2.tool.DepthFirstTerminate.getNumberOfThreads() has to be updated with a return value >1 to trigger the bug on Linux x86_64. On Windows, the bug does not seem reproducible regardless of getNumberOfThreads(). On Mac OSX, TLC can get stuck even with getNumberOfThreads() return 1.
Parallel TLC (workers > 1) reports intermittently an incorrect, too low diameter (length of the longest behavior found so far).
Commit f72e862 contains a test case that intermittently on Linux x86_64 reproduces the bug.
Also, the branch mku-trace-contention might have unintentionally fixed this. It changes the way how TLC handles the diameter internally.
Commit 3491467 introduces a new flag for TLC to defer liveness checking to after the (liveness) graph has been constructed. This is especially useful in situation where one assumes a spec is correct and thus does not need periodic liveness checking to catch liveness violations early.
Add a checkbox to the advanced options page of the model editor to activate deferred liveness checking. Additionally, we might want to revisit TLC's algorithm when to run periodic liveness checking.
...such as "Sun Dec 02 16:47:04 UTC 292269055". Starting TLC updates to the current time.
Taking a JFR flight recording of e.g. the OpenAddressing specification reveals that approximately 25% runtime are related to Context lookups. The corresponding lookup methods are tlatools/src/tlc2/util/Context.java#L46 and tlatools/src/tlc2/util/Context.java#L73. A yet to be invented lookup implementation can hopefully reduce this overhead.
Note that previous minor optimizations did not remove the bottleneck entirely (ef8acb9, 4366883, af4f9e2).
Below is a debug helper to print the maximal path in the context tree.
[...]
public final class Context {
private static final LongAccumulator CHAIN_LENGTH = new LongAccumulator(new LongBinaryOperator() {
public long applyAsLong(final long left, final long right) {
return Math.max(left, right);
}
}, 0);
[...]
public final Context cons(SymbolNode name, Object value) {
CHAIN_LENGTH.accumulate(this.length());
return new Context(name, value, this);
}
[...]
public final int length() {
// if (this.next == null) {
// return 0;
// }
int length = 0;
Context cur;
for (cur = this.next; cur != null; cur = cur.next) {
length++;
}
return length;
}
}
TLC seems to have problems performing the substitutions into subscripts. Consider the following specs
-------------------- MODULE Test -------------
EXTENDS Integers
VARIABLES y
I(x, c) == INSTANCE Test2
Init == I(y,0)!Init
Next == I(y,3)!Next
================================================
-------------- MODULE Test2 ---------------
EXTENDS Integers
CONSTANT c
VARIABLE x
Init == x = 0
Next == x'=(x+1) % c
SqNext == [Next]_x
BoxNext == [][Next]_x
Spec == Init /\ [][Next]_x
Fair == WF_x(Next)
===========================================
TLC can handle only the two checked properties
It produces an error on the next two, and SANY won’t parse the last property.
[Added by LL: ] SANY is correctly reporting an error in the last property, which is not syntactically correct.
I recently discovered a severe performance degradation caused by hotspot failing to optimize a hot method due to some uncommon syntax construct. In order to detect similar problems asap, JITWatch should be adopted.
Background reading:
http://normanmaurer.me/blog/2014/05/15/Inline-all-the-Things/
https://docs.oracle.com/javase/9/vm/compiler-control1.htm#JSJVM-GUID-94AD8194-786A-4F19-BFFF-278F8E237F3A
https://twitter.com/ErikGahlin/status/1207018011674185728
https://twitter.com/ErikGahlin/status/1207536016858505217
I've unpacked TLAToolbox-1.5.2-linux.gtk.x86_64.zip on my computer and attempted to launch it, but I am presented with an error shortly after the splash screen that directs me to a log file. The contents of this file are here, and seem to indicate missing dependencies.
Have I missed some installation instructions? It was my impression that this toolbox should have worked out-of-the-box...
I should note that this is a fairly recent Ubuntu desktop install, and in addition to out-of-the-box configuration I have installed openjdk and other assorted modules in attempts to get an unrelated IcedTea application installed. Attached is a file containing output from lsb_release, lscpu, and java -version.
I see instructions for setting up a development environment with Eclipse but not
for building a release package from the repository. When I try mvn install one of the
tests pops up an eclipse window and then fails when I close it. At that point the build is failed.
Let model editor make better use of screen estate. Especially:
xxyzz:
"If you run Model_1 of SendSetUndoPP, it will report an
Invariant TypeOKP is violated.
error and produces an error trace. Go to the end of the trace and double click on the last action (the one that produced the last state). You’ll see that it’s the SendP action on line 14 of SendSetUndoPP.tla. Now open the Error-Trace Exploration area and add the following two expressions:
SendP Send
These are action expressions, so they depend on variables and primed variables. The values of those expressions that apply to the final two states of the trace are reported with the next-to last state. Observe that SendP = FALSE. In other words, the trace explorer says that the final two states don’t satisfy SendP. However the error-trace also tells us that the last state was produced from the next-to last state by a SendP action.
-----------------------------------------------------------------------------
SendP2 == /\ Send
/\ ProphCondSend(p)
/\ p' \in NewProphs(p, Dom', DomInjSend, PredSetSend)
UndoP2 == /\ Undo
/\ ProphCondUndo(p)
/\ p' \in NewProphs(p, Dom', DomInjUndo, PredSetUndo)
NextP2 == (\E v \in Value: ChooseP(v)) \/ SendP2 \/ RcvP \/ UndoP2
SpecP2 == InitP /\ [][NextP2]_varsP
-----------------------------------------------------------------------------
I’ve defined SendP2 and UndoP2 by manually expanding the definition of NewProphecyAction in the definitions of SendP and Undo, and defined SpecP2 by replacing SendP and UndoP in SpecP with SendP2 and UndoP2. So SpecP and SpecP2 are obviously equivalent. Now clone Model_1 and in the resulting model, replace the specification SpecP with SpecP2. This time TLC runs correctly and finds no error. From the bogus error trace that SpecP produces, it looks like TLC is evaluating NewProphs incorrectly when it expands the definition of NewProphecyAction. Note that the ChooseP and RcvP actions are also defined in terms of NewProphecyAction, but they seem to work fine. The arguments with which NewProphecyAction is being called are defined starting on line 24 of SendSetUndo. The only significant difference between whether or not TLC is correctly evaluating NewProphecyAction and the others seems to be that it works incorrectly when a couple of the arguments have primes. However, all of them have the same argument Dom’."
YY: I would try to log as much as possible when getNextStates() is called on the preceding state that generates the bad state. I would use the fingerprint of that preceding state to do conditional logging.
I've been model checking a fairly large system, and have encountered odd behaviour when trying to run distributed TLC from the command line instead of the toolbox. I've been able to reproduce the same behaviour in a significantly smaller model which can be found at simu/tla-issue/model/fn.tla.
I've also included all scripts (simu/tla-issue/bin) and logs (simu/tla-issue/1.5.3, and simu/tla-issue/nightly-may16) of my experimentation in that repository.
Note that I've tried both TLAtoolbox release 1.5.3 (TLC 2.09) and the latest nightly (as of writing: e8e37a7, 2017-05-16, TLC 2.10) and the behaviour is identical.
The different behaviour can be characterized as follows:
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.10 of undefined (rev: e8e37a7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running in Model-Checking mode with 20 workers.
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file MC.tla
Parsing file fn.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module fn
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2017-05-18 11:02:56)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state generated.
@!@!@ENDMSG 2190 @!@!@
<< "slots:",
( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> TRUE] @@
1 :>
[ cap |-> "Null",
owner |-> NoOwner,
location |-> 1,
locked |-> FALSE ] ) >>
<< "slots'",
( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> FALSE] @@
1 :>
[ cap |-> "Null",
owner |-> NoOwner,
location |-> 1,
locked |-> FALSE ] ) >>
<< "slots:",
( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> FALSE] @@
1 :>
[ cap |-> "Null",
owner |-> NoOwner,
location |-> 1,
locked |-> FALSE ] ) >>
<< "slots'",
( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> FALSE] @@
1 :>
[ cap |-> "Null",
owner |-> NoOwner,
location |-> 1,
locked |-> FALSE ] ) >>
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 1.1E-19
based on the actual fingerprints: val = 1.5E-19
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2017-05-18 11:02:56
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 43, col 8 to line 49, col 35 of module fn: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(2) at 2017-05-18 11:02:56: 3 states generated (962 s/min), 2 distinct states found (641 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
3 states generated, 2 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 2.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 00s at (2017-05-18 11:02:56)
@!@!@ENDMSG 2186 @!@!@
Master process:
TLC2 TLC Server Version 2.10 of undefined
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file ../tla/debugging/fn.toolbox/Model_1/MC.tla
Parsing file ../tla/debugging/fn.toolbox/Model_1/fn.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module fn
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2017-05-18 11:01:24)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state(s) generated.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 7000:0 @!@!@
TLC server at sgd-dalcoi7-09 is ready (2017-05-18 11:01:24)
@!@!@ENDMSG 7000 @!@!@
@!@!@STARTMSG 7001:0 @!@!@
Registration for worker at rmi://sgd-dalcoi7-09:40553/1 completed (2017-05-18 11:01:27)
@!@!@ENDMSG 7001 @!@!@
@!@!@STARTMSG 7001:0 @!@!@
Registration for worker at rmi://sgd-dalcoi7-09:40553/3 completed (2017-05-18 11:01:27)
@!@!@ENDMSG 7001 @!@!@
@!@!@STARTMSG 7001:0 @!@!@
Registration for worker at rmi://sgd-dalcoi7-09:40553/2 completed (2017-05-18 11:01:27)
@!@!@ENDMSG 7001 @!@!@
@!@!@STARTMSG 7001:0 @!@!@
Registration for worker at rmi://sgd-dalcoi7-09:40553/0 completed (2017-05-18 11:01:27)
@!@!@ENDMSG 7001 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
slots = ( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> TRUE] @@
1 :> [cap |-> "Null", owner |-> NoOwner, location |-> 1, locked |-> FALSE] )
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 7003:0 @!@!@
Worker: rmi://sgd-dalcoi7-09:40553/1 Sent: 1 Rcvd: 0 CacheRatio: 1.00 (2017-05-18 11:01:27)
@!@!@ENDMSG 7003 @!@!@
@!@!@STARTMSG 7003:0 @!@!@
Worker: rmi://sgd-dalcoi7-09:40553/2 Sent: 0 Rcvd: 0 CacheRatio: 1.00 (2017-05-18 11:01:27)
@!@!@ENDMSG 7003 @!@!@
@!@!@STARTMSG 7003:0 @!@!@
Worker: rmi://sgd-dalcoi7-09:40553/3 Sent: 0 Rcvd: 0 CacheRatio: 1.00 (2017-05-18 11:01:27)
@!@!@ENDMSG 7003 @!@!@
@!@!@STARTMSG 7003:0 @!@!@
Worker: rmi://sgd-dalcoi7-09:40553/0 Sent: 0 Rcvd: 0 CacheRatio: 1.00 (2017-05-18 11:01:27)
@!@!@ENDMSG 7003 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(1) at 2017-05-18 11:01:27: 1 states generated (0 s/min), 1 distinct states found (0 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
1 states generated, 1 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 03s at (2017-05-18 11:01:27)
@!@!@ENDMSG 2186 @!@!@
@!@!@STARTMSG 2211:0 @!@!@
sgd-dalcoi7-09, work completed. Thank you!
@!@!@ENDMSG 2211 @!@!@
Worker process:
TLC Worker Version 2.10 of undefined
Parsing file /tmp/1495098087371/MC.tla
Parsing file /tmp/1495098087371/fn.tla
Parsing file /tmp/1495098087371/TLC.tla
Parsing file /tmp/1495098087371/Naturals.tla
Parsing file /tmp/1495098087371/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module TLC
Semantic processing of module fn
Semantic processing of module MC
Starting... (2017-05-18 11:01:27)
TLC worker with 4 threads ready at: Thu May 18 11:01:27 CEST 2017
<< "slots:",
( 0 :> [cap |-> "Mem", owner |-> 0, location |-> 0, locked |-> TRUE] @@
1 :>
[ cap |-> "Null",
owner |-> NoOwner,
location |-> 1,
locked |-> FALSE ] ) >>
sgd-dalcoi7-09, work completed at: Thu May 18 11:01:27 CEST 2017 Computed: 0 and a cache hit ratio of 1, Thank you!
sgd-dalcoi7-09, work completed at: Thu May 18 11:01:27 CEST 2017 Computed: 0 and a cache hit ratio of 1, Thank you!
sgd-dalcoi7-09, work completed at: Thu May 18 11:01:27 CEST 2017 Computed: 0 and a cache hit ratio of 1, Thank you!
sgd-dalcoi7-09, work completed at: Thu May 18 11:01:27 CEST 2017 Computed: 0 and a cache hit ratio of 1, Thank you!
Choose x \in A : P" is a nice construct that allows to express ideas succinctly but
TLC evaluates it that way: it generates all the elements in A and then filter them using P.
If A is large, an exception is thrown.A better way to evaluate the construct would be to generate an element of A, check that P is true,
if yes stop the algorithm in the other case continue. Obviously we can get too long a loop in that
case but in the better case we can have the opportunity to find the right element in a decent
time interval which cannot happen with the current algorithm. (Obviously if the loop is too
long we need a way to stop it.)Generating one element at a time and then visiting it, is
the basic philosophy to evaluate combinatorial objects such as all trees or all permutations favored
by Knuth in TAOCP 4A.
The spec below can be used to debug CHOOSE:
------------------------------- MODULE Choose -------------------------------
EXTENDS Naturals, TLC
CONSTANT S
VARIABLE x
Init == x = 0
Next == /\ PrintT(CHOOSE s \in S : s > 0)
/\ UNCHANGED<<x>>
Spec == Init /\ Next
===================
xxyzz:
CHOOSE is implemented the way it is to ensure that S = T implies CHOOSE x \in S : P(x) = CHOOSE x \in T : P(x).
The only way I know to ensure this property is to evaluate the set and put it in normal form before choosing an element from it.
I recently upgraded my TLA Toolbox installation using the internal updater from version 1.5.2 to 1.5.3 and attempted to use the new cloud TLC feature with Azure, following the instructions to generate certificates and set the relevant environment variables.
Upon clicking the run button, nothing appeared to happen, so as per the help file I ran the toolbox with -console and -consolelog. The console spawned has a limited scrollback buffer but I have copied what I could and attached the log.
The error message asks me to look to see if the "JCloud distributed TLC provider" is installed, and if not, to report a bug. I found a component with a similar name, but not one with that exact name. I've attached a screenshot.
ahelwer:
Windows 8.1 on Surface Pro 3, resolution 2160 x 1440.
xxyzz:
If you use Definition Override to override a defined quantify by a model value, the background color of the text box for specifying the new definition turns gray and the box becomes read-only. However, the text is left in the box. This is a bug. When close the override window and then edit the override, it usually shows something like this:
However, the text box is editable. This is a bug; it should be read-only. For consistency, it might be nice if the “Infinity” had been placed in the box when Model value was originally selected.
Now the problem. (You can use the attached spec MinMax1 to check all this out.) Suppose that the definition being replaced was the definition of M!Infinity which was imported into the current module with
M == INSTANCE MinMax2 WITH ...
Then what opening the override for editing shows is this:
This is misleading because it’s really the definition of M!Infinity that’s being replaced by the model value Infinity. In both cases, the list of overrides in the Definition Override section of the page shows
so there can be multiple such entries that look identical, and you have to open them to see which is which. But things can be worse. Suppose M!Infinity were instantiated by an ordinary assignment, then you see something like this:
If the spec contained the two statements
M == INSTANCE MinMax2 WITH ...
N == INSTANCE MinMax2 WITH ...
then you can’t see whether it’s M!Infinity or N!Infinity whose definition is being overridden. (You’d have to select Model value, close the override and then edit it.)
Here’s what I think should be done. If the definition one is overriding is the definition of M!Infinity, then the override window should show
M!Infinity <-
and, for a model value instantiation, the list of all overrides should show
M!Infinity <- [model value] Infinity
When you click on the Add button, the list of definitions should show Infinity and M!Infinity (and N!Infinity if that’s defined). And you should be able to type M!Infinity in the search box. However, if you type Infinity into the search box, then it should present Infinity, M!Infinity, and N!Infinity as possible choices.
mateusbraga:
The image shows my invariant and the error message I get. The result of the error-trace is as expected, but the error message on the top-right is incorrect.
Context: Previously I had the invariant b = 3, which I changed to b # 4 later.
LL: "I tried opening a spec and it opened with a "Failed to create the part's controls" error, which seemed to be caused by an inability to open the root module. It was a garbage spec, and I thought I had probably deleted the root module, so I deleted the spec. I then tried to open a new spec with the same root module. It created the spec but produced the same error, with the “details” appended below. I observed that the root file actually did exist. Also, in the file explorer, the list of modules includes both the root file (Test.tla) and an EXTENDed library module (TLAPS.tla), indicating that the root module was successfully parsed. Double-clicking on TLAPS in the spec explorer opened that file, but double-clicking on the root module produced the same error. So I deleted the spec again and then deleted the root file and opened a new spec by the same name. It was aware that the specified root file did not exist, but it still produced the same error. I’ve attached the two files that were in the .toolbox directory. I then deleted the spec, closed the Toolbox, re-opened it, and tried again to create the new spec Test. This time it worked."
java.lang.IllegalArgumentException: Argument not valid at org.eclipse.swt.SWT.error(SWT.java:4472) at org.eclipse.swt.SWT.error(SWT.java:4406) at org.eclipse.swt.SWT.error(SWT.java:4377) at org.eclipse.swt.custom.StyledText.setStyleRanges(StyledText.java:9885) at org.eclipse.swt.custom.StyledText.setStyleRanges(StyledText.java:9979) at org.eclipse.jface.text.TextViewer.applyTextPresentation(TextViewer.java:4884) at org.eclipse.jface.text.TextViewer.changeTextPresentation(TextViewer.java:4936) at org.eclipse.jface.text.presentation.PresentationReconciler.applyTextRegionCollection(PresentationReconciler.java:582) at org.eclipse.jface.text.presentation.PresentationReconciler.processDamage(PresentationReconciler.java:571) at org.eclipse.jface.text.presentation.PresentationReconciler.access$3(PresentationReconciler.java:567) at org.eclipse.jface.text.presentation.PresentationReconciler$InternalListener.inputDocumentChanged(PresentationReconciler.java:119) at org.eclipse.jface.text.TextViewer.fireInputDocumentChanged(TextViewer.java:2890) at org.eclipse.jface.text.TextViewer.setDocument(TextViewer.java:2939) at org.eclipse.jface.text.source.SourceViewer.setDocument(SourceViewer.java:643) at org.eclipse.jface.text.source.projection.ProjectionViewer.setDocument(ProjectionViewer.java:375) at org.eclipse.jface.text.source.SourceViewer.setDocument(SourceViewer.java:591) at org.eclipse.ui.texteditor.AbstractTextEditor.initializeSourceViewer(AbstractTextEditor.java:4050) at org.eclipse.ui.texteditor.AbstractTextEditor.createPartControl(AbstractTextEditor.java:3578) at org.eclipse.ui.texteditor.StatusTextEditor.createPartControl(StatusTextEditor.java:54) at org.eclipse.ui.texteditor.AbstractDecoratedTextEditor.createPartControl(AbstractDecoratedTextEditor.java:447) at org.lamport.tla.toolbox.editor.basic.TLAEditor.createPartControl(TLAEditor.java:302) at org.eclipse.ui.part.MultiPageEditorPart.addPage(MultiPageEditorPart.java:244) at org.eclipse.ui.forms.editor.FormEditor.addPage(FormEditor.java:325) at org.lamport.tla.toolbox.editor.basic.TLAEditorAndPDFViewer.addPages(TLAEditorAndPDFViewer.java:79) at org.eclipse.ui.forms.editor.FormEditor.createPages(FormEditor.java:138) at org.eclipse.ui.part.MultiPageEditorPart.createPartControl(MultiPageEditorPart.java:363) at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.createPartControl(CompatibilityPart.java:151) at org.eclipse.ui.internal.e4.compatibility.CompatibilityEditor.createPartControl(CompatibilityEditor.java:99) at org.eclipse.ui.internal.e4.compatibility.CompatibilityPart.create(CompatibilityPart.java:341) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source) at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source) at java.lang.reflect.Method.invoke(Unknown Source) at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56) at org.eclipse.e4.core.internal.di.InjectorImpl.processAnnotated(InjectorImpl.java:898) at org.eclipse.e4.core.internal.di.InjectorImpl.processAnnotated(InjectorImpl.java:879) at org.eclipse.e4.core.internal.di.InjectorImpl.inject(InjectorImpl.java:121) at org.eclipse.e4.core.internal.di.InjectorImpl.internalMake(InjectorImpl.java:345) at org.eclipse.e4.core.internal.di.InjectorImpl.make(InjectorImpl.java:264) at org.eclipse.e4.core.contexts.ContextInjectionFactory.make(ContextInjectionFactory.java:162) at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.createFromBundle(ReflectionContributionFactory.java:104) at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.doCreate(ReflectionContributionFactory.java:73) at org.eclipse.e4.ui.internal.workbench.ReflectionContributionFactory.create(ReflectionContributionFactory.java:55) at org.eclipse.e4.ui.workbench.renderers.swt.ContributedPartRenderer.createWidget(ContributedPartRenderer.java:129) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.createWidget(PartRenderingEngine.java:971) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.safeCreateGui(PartRenderingEngine.java:640) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.safeCreateGui(PartRenderingEngine.java:746) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.access$0(PartRenderingEngine.java:717) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$2.run(PartRenderingEngine.java:711) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.createGui(PartRenderingEngine.java:695) at org.eclipse.e4.ui.internal.workbench.PartServiceImpl$1.handleEvent(PartServiceImpl.java:99) at org.eclipse.e4.ui.services.internal.events.UIEventHandler$1.run(UIEventHandler.java:40) at org.eclipse.swt.widgets.Synchronizer.syncExec(Synchronizer.java:186) at org.eclipse.ui.internal.UISynchronizer.syncExec(UISynchronizer.java:145) at org.eclipse.swt.widgets.Display.syncExec(Display.java:4761) at org.eclipse.e4.ui.internal.workbench.swt.E4Application$1.syncExec(E4Application.java:211) at org.eclipse.e4.ui.services.internal.events.UIEventHandler.handleEvent(UIEventHandler.java:36) at org.eclipse.equinox.internal.event.EventHandlerWrapper.handleEvent(EventHandlerWrapper.java:197) at org.eclipse.equinox.internal.event.EventHandlerTracker.dispatchEvent(EventHandlerTracker.java:197) at org.eclipse.equinox.internal.event.EventHandlerTracker.dispatchEvent(EventHandlerTracker.java:1) at org.eclipse.osgi.framework.eventmgr.EventManager.dispatchEvent(EventManager.java:230) at org.eclipse.osgi.framework.eventmgr.ListenerQueue.dispatchEventSynchronous(ListenerQueue.java:148) at org.eclipse.equinox.internal.event.EventAdminImpl.dispatchEvent(EventAdminImpl.java:135) at org.eclipse.equinox.internal.event.EventAdminImpl.sendEvent(EventAdminImpl.java:78) at org.eclipse.equinox.internal.event.EventComponent.sendEvent(EventComponent.java:39) at org.eclipse.e4.ui.services.internal.events.EventBroker.send(EventBroker.java:85) at org.eclipse.e4.ui.internal.workbench.UIEventPublisher.notifyChanged(UIEventPublisher.java:59) at org.eclipse.emf.common.notify.impl.BasicNotifierImpl.eNotify(BasicNotifierImpl.java:374) at org.eclipse.e4.ui.model.application.ui.impl.ElementContainerImpl.setSelectedElement(ElementContainerImpl.java:171) at org.eclipse.e4.ui.internal.workbench.ModelServiceImpl.showElementInWindow(ModelServiceImpl.java:572) at org.eclipse.e4.ui.internal.workbench.ModelServiceImpl.bringToTop(ModelServiceImpl.java:536) at org.eclipse.e4.ui.internal.workbench.PartServiceImpl.delegateBringToTop(PartServiceImpl.java:724) at org.eclipse.e4.ui.internal.workbench.PartServiceImpl.bringToTop(PartServiceImpl.java:396) at org.eclipse.e4.ui.internal.workbench.PartServiceImpl.showPart(PartServiceImpl.java:1166) at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditor(WorkbenchPage.java:3252) at org.eclipse.ui.internal.WorkbenchPage.access$25(WorkbenchPage.java:3167) at org.eclipse.ui.internal.WorkbenchPage$10.run(WorkbenchPage.java:3149) at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70) at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3144) at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3108) at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:3089) at org.lamport.tla.toolbox.util.UIHelper.openEditor(UIHelper.java:352) at org.lamport.tla.toolbox.ui.handler.OpenSpecHandler$1$1.runInUIThread(OpenSpecHandler.java:79) at org.eclipse.ui.progress.UIJob$1.run(UIJob.java:97) at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35) at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135) at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4155) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3772) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018) at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156) at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606) at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150) at org.lamport.tla.toolbox.Application.start(Application.java:77) at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source) at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source) at java.lang.reflect.Method.invoke(Unknown Source) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608) at org.eclipse.equinox.launcher.Main.run(Main.java:1515) at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
A ghost remains after Model_4 is deleted (see image below). As a workaround, closing and re-opening the specification removes the ghost model.
The Eclipse console shows:
org.eclipse.debug.core.DebugException: Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
at org.eclipse.debug.internal.core.LaunchManager.createDebugException(LaunchManager.java:930)
at org.eclipse.debug.internal.core.LaunchManager.getInfo(LaunchManager.java:1400)
at org.eclipse.debug.internal.core.LaunchConfiguration.getInfo(LaunchConfiguration.java:470)
at org.eclipse.debug.internal.core.LaunchConfiguration.getAttribute(LaunchConfiguration.java:416)
at org.lamport.tla.toolbox.tool.tlc.model.Model.getName(Model.java:245)
at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelLabelProvider.getText(ModelLabelProvider.java:57)
at org.eclipse.ui.internal.navigator.extensions.SafeDelegateCommonLabelProvider.getText(SafeDelegateCommonLabelProvider.java:112)
at org.eclipse.ui.internal.navigator.extensions.SafeDelegateCommonLabelProvider.getStyledText(SafeDelegateCommonLabelProvider.java:120)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceLabelProvider.findStyledText(NavigatorContentServiceLabelProvider.java:167)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceLabelProvider.getStyledText(NavigatorContentServiceLabelProvider.java:153)
at org.eclipse.ui.internal.navigator.NavigatorDecoratingLabelProvider$StyledLabelProviderAdapter.getStyledText(NavigatorDecoratingLabelProvider.java:63)
at org.eclipse.jface.viewers.DelegatingStyledCellLabelProvider.getStyledText(DelegatingStyledCellLabelProvider.java:206)
at org.eclipse.jface.viewers.DecoratingStyledCellLabelProvider.getStyledText(DecoratingStyledCellLabelProvider.java:199)
at org.eclipse.jface.viewers.DelegatingStyledCellLabelProvider.update(DelegatingStyledCellLabelProvider.java:106)
at org.eclipse.jface.viewers.DecoratingStyledCellLabelProvider.update(DecoratingStyledCellLabelProvider.java:136)
at org.eclipse.jface.viewers.ViewerColumn.refresh(ViewerColumn.java:154)
at org.eclipse.jface.viewers.AbstractTreeViewer.doUpdateItem(AbstractTreeViewer.java:949)
at org.eclipse.jface.viewers.AbstractTreeViewer$UpdateItemSafeRunnable.run(AbstractTreeViewer.java:114)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:50)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:173)
at org.eclipse.jface.viewers.AbstractTreeViewer.doUpdateItem(AbstractTreeViewer.java:1029)
at org.eclipse.jface.viewers.StructuredViewer$UpdateItemSafeRunnable.run(StructuredViewer.java:473)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:50)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:173)
at org.eclipse.jface.viewers.StructuredViewer.updateItem(StructuredViewer.java:2176)
at org.eclipse.jface.viewers.StructuredViewer.internalUpdate(StructuredViewer.java:2159)
at org.eclipse.jface.viewers.StructuredViewer.update(StructuredViewer.java:2097)
at org.eclipse.jface.viewers.ColumnViewer.update(ColumnViewer.java:541)
at org.eclipse.ui.navigator.CommonViewer.update(CommonViewer.java:510)
at org.eclipse.jface.viewers.StructuredViewer.update(StructuredViewer.java:2041)
at org.eclipse.jface.viewers.StructuredViewer.handleLabelProviderChanged(StructuredViewer.java:1208)
at org.eclipse.ui.navigator.CommonViewer.handleLabelProviderChanged(CommonViewer.java:236)
at org.eclipse.jface.viewers.ContentViewer$1.labelProviderChanged(ContentViewer.java:99)
at org.eclipse.jface.viewers.BaseLabelProvider$1.run(BaseLabelProvider.java:72)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:50)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:173)
at org.eclipse.jface.viewers.BaseLabelProvider.fireLabelProviderChanged(BaseLabelProvider.java:69)
at org.eclipse.jface.viewers.DecoratingStyledCellLabelProvider$1.labelProviderChanged(DecoratingStyledCellLabelProvider.java:78)
at org.eclipse.ui.internal.decorators.DecoratorManager$1.run(DecoratorManager.java:446)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.decorators.DecoratorManager.fireListener(DecoratorManager.java:443)
at org.eclipse.ui.internal.decorators.DecorationScheduler$3.runInUIThread(DecorationScheduler.java:536)
at org.eclipse.ui.progress.UIJob$1.run(UIJob.java:97)
at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4155)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3772)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
at org.lamport.tla.toolbox.Application.start(Application.java:77)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)
at org.eclipse.equinox.launcher.Main.run(Main.java:1515)
at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
!SUBENTRY 1 org.eclipse.debug.core 4 5012 2016-12-11 12:37:24.318
!MESSAGE Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
Clicking on the ghost icon (with blank name) produced the following exception:
!ENTRY org.lamport.tla.toolbox.tool.tlc 4 0 2016-12-11 12:41:51.857
!MESSAGE Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
!STACK 1
org.eclipse.debug.core.DebugException: Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
at org.eclipse.debug.internal.core.LaunchManager.createDebugException(LaunchManager.java:930)
at org.eclipse.debug.internal.core.LaunchManager.getInfo(LaunchManager.java:1400)
at org.eclipse.debug.internal.core.LaunchConfiguration.getInfo(LaunchConfiguration.java:470)
at org.eclipse.debug.internal.core.LaunchConfiguration.getAttribute(LaunchConfiguration.java:416)
at org.lamport.tla.toolbox.tool.tlc.model.Model.getComments(Model.java:254)
at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelLabelProvider.getDescription(ModelLabelProvider.java:77)
at org.eclipse.ui.internal.navigator.extensions.SafeDelegateCommonLabelProvider.getDescription(SafeDelegateCommonLabelProvider.java:79)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceDescriptionProvider.getDescription(NavigatorContentServiceDescriptionProvider.java:66)
at org.eclipse.ui.navigator.CommonNavigatorManager.updateStatusBar(CommonNavigatorManager.java:321)
at org.eclipse.ui.navigator.CommonNavigatorManager$1.selectionChanged(CommonNavigatorManager.java:75)
at org.eclipse.jface.viewers.StructuredViewer$3.run(StructuredViewer.java:877)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:50)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:173)
at org.eclipse.jface.viewers.StructuredViewer.firePostSelectionChanged(StructuredViewer.java:874)
at org.eclipse.jface.viewers.StructuredViewer.handlePostSelect(StructuredViewer.java:1243)
at org.eclipse.ui.navigator.CommonViewer.handlePostSelect(CommonViewer.java:455)
at org.eclipse.jface.viewers.StructuredViewer$5.widgetSelected(StructuredViewer.java:1269)
at org.eclipse.jface.util.OpenStrategy.firePostSelectionEvent(OpenStrategy.java:265)
at org.eclipse.jface.util.OpenStrategy.access$5(OpenStrategy.java:259)
at org.eclipse.jface.util.OpenStrategy$1$2.run(OpenStrategy.java:440)
at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4155)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3772)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
at org.lamport.tla.toolbox.Application.start(Application.java:77)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)
at org.eclipse.equinox.launcher.Main.run(Main.java:1515)
at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
!SUBENTRY 1 org.eclipse.debug.core 4 5012 2016-12-11 12:41:51.858
!MESSAGE Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
!ENTRY org.lamport.tla.toolbox.tool.tlc 4 0 2016-12-11 12:41:51.870
!MESSAGE Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
!STACK 1
org.eclipse.debug.core.DebugException: Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
at org.eclipse.debug.internal.core.LaunchManager.createDebugException(LaunchManager.java:930)
at org.eclipse.debug.internal.core.LaunchManager.getInfo(LaunchManager.java:1400)
at org.eclipse.debug.internal.core.LaunchConfiguration.getInfo(LaunchConfiguration.java:470)
at org.eclipse.debug.internal.core.LaunchConfiguration.getAttribute(LaunchConfiguration.java:416)
at org.lamport.tla.toolbox.tool.tlc.model.Model.getName(Model.java:245)
at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelLabelProvider.getText(ModelLabelProvider.java:57)
at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelLabelProvider.getDescription(ModelLabelProvider.java:79)
at org.eclipse.ui.internal.navigator.extensions.SafeDelegateCommonLabelProvider.getDescription(SafeDelegateCommonLabelProvider.java:79)
at org.eclipse.ui.internal.navigator.NavigatorContentServiceDescriptionProvider.getDescription(NavigatorContentServiceDescriptionProvider.java:66)
at org.eclipse.ui.navigator.CommonNavigatorManager.updateStatusBar(CommonNavigatorManager.java:321)
at org.eclipse.ui.navigator.CommonNavigatorManager$1.selectionChanged(CommonNavigatorManager.java:75)
at org.eclipse.jface.viewers.StructuredViewer$3.run(StructuredViewer.java:877)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:50)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:173)
at org.eclipse.jface.viewers.StructuredViewer.firePostSelectionChanged(StructuredViewer.java:874)
at org.eclipse.jface.viewers.StructuredViewer.handlePostSelect(StructuredViewer.java:1243)
at org.eclipse.ui.navigator.CommonViewer.handlePostSelect(CommonViewer.java:455)
at org.eclipse.jface.viewers.StructuredViewer$5.widgetSelected(StructuredViewer.java:1269)
at org.eclipse.jface.util.OpenStrategy.firePostSelectionEvent(OpenStrategy.java:265)
at org.eclipse.jface.util.OpenStrategy.access$5(OpenStrategy.java:259)
at org.eclipse.jface.util.OpenStrategy$1$2.run(OpenStrategy.java:440)
at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:35)
at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:135)
at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:4155)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3772)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018)
at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
at org.lamport.tla.toolbox.Application.start(Application.java:77)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608)
at org.eclipse.equinox.launcher.Main.run(Main.java:1515)
at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
!SUBENTRY 1 org.eclipse.debug.core 4 5012 2016-12-11 12:41:51.872
!MESSAGE Launch configuration DieHard___Model_4 at file:/C:/lamport/talks/microsoft16/DieHard.toolbox/DieHard___Model_4.launch does not exist.
The Toolbox creates its corresponding workspace directory in the current directory from where it was launched. Unless users start the Toolbox via a static mechanism like the start menu or app launcher, they tend to end up with several workspaces. A newly created workspace has no references to existing specs and the Toolbox appears to have forgotten all specs.
Adding the property [email protected]/.tlaplus to the product file will cause the workspace to universally be created in the user's home directory regardless of the actual path from where it's started. However, we have to tell our existing users to manually move their existing workspace to @user.home/.tlaplus once.
The current .deb Toolbox package sets osgi.instance.area.default already. This has to be removed with the change to the product file.
I simply cannot create any new Specs with Add new Spec menu because it fails always with the following error:
An internal error occurred during: "NewSpecWizard job".
assertion failed: E:\temp\tla-test-spec\testspec.toolbox is *not* a subdirectory of e:\temp\tla-test-spec\testspec.tla. This is commonly caused by a symlink contained in the latter path.
Please note that there are no symlinks involved anywhere.
When TLC recovers from a checkpoint, initial states are not recovered/re-created. Liveness checking however works by exploring (prefixes of) behaviors (which each obviously starts at an initial state). Without initial states, TLC silently skips liveness checking (see LiveWorker). As a consequence, liveness violations can be missed when TLC is run from a checkpoint.
This problem can be reproduce with CodePlexBug08EWD840FL2Test:
public CodePlexBug08EWD840FL2FromCheckpointTest() { super("EWD840MC2", "CodePlexBug08", new String[] {"-recover", BASE_DIR + TEST_MODEL + "CodePlexBug08" + File.separator + "checkpoint"}); } Error running tlapm. Report a bug with the error code to the developers at https://tlaplus.codeplex.com/workitem/list/basic.
Error code: -1073741515
Well, I think I have installed the toolbox and tlaps just following the steps on the toolbox's web page, but still couldn't run tlapm or even launch provers. Have I done something wrong with it?
Error code and the screenshot is attached above. Please help me with the problem, thx :)
I've tried a couple releases (1.4.5-linux.gtk.x86_64 and 1.5.2-linux.gtk.x86_64)
Upon trying to create and open a new spec, I hit a null pointer:
An internal error occurred during: "OpenSpecHandler is parsing spec...".
java.lang.NullPointerException
Using openjdk-8-jre on a recent Ubuntu derivative
I will happily provide more information if somebody can guide me to it
Code:
EXTENDS TLC
VARIABLES x
Next == Assert(x = TRUE, "Failed") /\ UNCHANGED x
Init == x = CASE TRUE -> TRUE
[] TRUE -> FALSE
Spec == Init /\ [][Next]_x
Expected: Spec fails.
Actual: Spec passes.
Notes: If we replace Init with x = CHOOSE p \in BOOLEAN : (TRUE /\ p = TRUE) \/ (TRUE /\ p = FALSE), as per formal semantics on 298 of Specifying Systems, the spec fails as expected.
If a function is defined with the syntax f[x \in S \X S] == ... but is applied to multiple arguments f[x, y], then SANY (from version 1.5.3 of the TLAtoolbox) reports an error about arity mismatch:
Function 'f' is defined with 1 parameters, but is applied to 2 arguments.
I understand that the motivation for raising an error in this case is to avoid what will usually indicate
a reasoning error. Based on my understanding of TLA+ (see also example below) this seems valid TLA+ (p.303 in the TLA+ book and the untyped nature of TLA+). One possibility could be for SANY to raise a warning instead of an error for this case.
The function application can always be rewritten equivalently without syntactic sugar as f[ << a, b >> ], thus avoiding the SANY error. So raising this error does not restrict what one can express.
As an example of the behavior described above, invoking java -cp /some/path/tlatools/tla/ -DTLA-Library=/some/other/path/v2-tlapm/library tla2sany.SANY test.tla with the following module:
------------------------------- MODULE test ------------------------------------
EXTENDS FiniteSets
LEMMA
ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
PROVE LET f == [x \in S \X S |-> e(x[1], x[2])]
IN \A x \in S : IsFiniteSet({f[x,y] : y \in S})
LEMMA
ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
PROVE LET f[x \in S \X S] == e(x[1], x[2])
IN \A x \in S : IsFiniteSet({f[x,y] : y \in S})
================================================================================produces the output:
****** SANY2 Version 2.1 created 24 February 2014
Parsing file test.tla
Parsing file /some/other/path/v2-tlapm/library/FiniteSets.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module test
Semantic errors:
*** Errors: 1
line 14, col 40 to line 14, col 45 of module test
Function 'f' is defined with 1 parameters, but is applied to 2 arguments.
So SANY indicates that the function application in the second lemma is in error, even though tlapm (version 1.4.3) proves that the functions in the two lemmata are equal (as described on p.304 of the TLA+ book):
LEMMA
ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
PROVE LET
f1 == [x \in S \X S |-> e(x[1], x[2])]
f2[x \in S \X S] == e(x[1], x[2])
IN f1 = f2
OBVIOUSThe SANY error message appears to originate from
: // If the function appears with numArgs >= 2 argument
// expressions, it must be declared with exactly numArgs
// parameters; and a function with numParms parameters in
// its definition should be applied to exactly numParms
// expressions, or 1 expression (representing arguments in
// tuple form), or 0 expressions (representing the
// function itself). Note: one cannot define a function
// with 0 arguments in TLA+.
if ( numArgs >= 2 && numParms != numArgs ) {
errors.addError(treeNode.getLocation(),
"Function '" +
((OpApplNode)sns[0]).getOperator().getName() +
"' is defined with " + numParms +
" parameters, but is applied to " +
numArgs + " arguments.");
return nullOAN;This issue was first discussed in this thread.
The PTL backend of TLAPS can be tricked into believing that an obligation appears in a []-context when in fact it does not. A primed state formula can then be "proved" using PTL when the corresponding unprimed formula is available as an assumption. The following module illustrates the bug.
---- MODULE Error ----
EXTENDS Naturals
VARIABLE xyz
Init == xyz = 0
Inc(x) == xyz' = xyz+x
Next == \E x \in Nat : Inc(x)
Spec == Init /\ [][Next]_xyz
LEMMA Spec => []Init
<1>1. Init /\ [Next]_xyz => Init'
<2>. SUFFICES ASSUME Init, Next PROVE Init' BY DEF Init
(* the following step illustrates the error and should not be provable *)
<2>1. ASSUME NEW x \in Nat, Inc(x) PROVE Init' BY PTL
<2>. QED BY <2>1 DEF Next
<1>. QED BY <1>1, PTL DEF Spec
===============================
@xxyzzn: "A counterexample to a liveness property must be an infinite trace. A error trace that TLC finds consists of a finite trace that loops back on itself --- indicated by a finite trace followed either by something like <Back to state 7> or . However, if you run the trace explorer, that looping indication is [incorrectly put at the top/bottom of the error trace]. The workaround is simple: just remember how it loops before running the trace explorer. If you forget to do that, the Trace Explorer's "Restore" button will put back the original error trace."
Code pointers:
org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCError.java
org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TraceExplorerDataProvider.java
libal:
Since the exporting is done after semantic parsing, a big amount of information is not important (such as auxialiary variables used for level computation). one such information, in my opinion, is the ThmOrAssumpNode which is the name associated with theorems and assumptions. in the XML exporter, I have normalized it out by referring directly to its theorems and asumptions.
The change I have made is to associate each such node with the theorem or assumption it is referring to. I made this associatation in the constructor of the theorem or assumption because each theorem or assumption has (if named) a link to this object. So I just doubled the link.
This change seems to work fine until (i think) there is an instantiation of theorems or assumptions, such as in:
line 952, col 1 to line 952, col 46 of module BPConProof_testIn this case, the link between a ThmOrAssumpNode and its TheoremNode is severed and my model breaks because such links are crucial. I believe this is because, under instantiations, the ThmOrAssumpNode was changed.
Still, it doesnt seem appropriate to me that definitions of theorems in the semantic tree exist without the theorems as I get ThmOrAssumpNode objects which were never given as input to theorms (and therefore the double link was not created) (btw, the objects were not marked as private but I tried also with private ThmOrAssumpNode fields to the same affect).
Anyway, I would like your advice about this problem in SANY and to log here that it should be fixed.
I encountered this problem in the BPConProof_test only and not in other tla modules I have tested.
Our code signing certificate has expired. We cannot sign the worker code which causes Java Webstart to complain.
The following commands should run as part of the instance provisioning in https://github.com/tlaplus/tlaplus/blob/master/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java
Disable hugepage defragmentation (especially important on highmem instances):
echo never > /sys/kernel/mm/transparent_hugepage/defrag
Turn off NUMA balancing:
echo 0 > /proc/sys/kernel/numa_balancing
Optimize fs towards performance sacrificing data durability
mkfs.ext4 -O ^has_journal /dev/md0
Ramdisk for states/ directory on highmem instances
mount -t ramfs ramfs /path/to/spec/
Disable OOM killer
sysctl vm.overcommit_memory=2
What: Clone the current model, when TLC is run.
Use case: Compare TLC runs WRT the spec and model parameters.
Nice to have: Add support to compare models with Eclipse's history view.
xxyzzn:
It is impossible to override the definition of the infix operator !! . Trying to override it produces an error in the files with which the Toolbox runs TLC. Furthermore, it is impossible to select the following operators using the search box in the Select Definition to Override window: * * ?? < . I suspect that "" and "?" are wildcards for the search. These operators can be overridden by clicking on them in that window.
This happens in two cases:
see for example: text-model/parsing/test206.tla
see for example: test-models/parsing/test217.tla
given module:
EXTENDS Integers
df(x) == CASE x < 0 -> -1
[] x = 0 -> 0
[] OTHER -> 1
debugging using the explorer:
tlaplus/tlatools/dist$ java -cp tla2tools.jar tla2sany.SANY -d ~/Documents/tla/repository/trunk/v2-tlapm/Toy.tla
gives:
*OpDefNode: df
uid: 255 kind: UserDefinedOpKind arity: 1 orgDefInModule: Toy
local: false
letInLevel: 0
inRecursive: false
inRecursiveSection: false
recursiveSection: -1
local: false
source: this
originallyDefinedInModule: Toy (uid: 239)
Formal params: 1
| | *FormalParamNode: x uid: 240 kind: FormalParamKind arity: 0
SymbolTable: non-null
| Body:
| | *OpApplNode: $Case uid: 254 kind: OpApplKind errors: non-null
| | | Operator: $Case 82
| | | Operands: 3
| | | | *OpApplNode: $Pair uid: 246 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | *OpApplNode: < uid: 243 kind: OpApplKind errors: non-null
| | | | | | *OpApplNode: -. uid: 245 kind: OpApplKind errors: non-null
| | | | *OpApplNode: $Pair uid: 251 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | *OpApplNode: = uid: 249 kind: OpApplKind errors: non-null
| | | | | | *NumeralNode: uid: 250 kind: NumeralKind Value: 0; image: 0
| | | | *OpApplNode: $Pair uid: 253 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | null
| | | | | | *NumeralNode: uid: 252 kind: NumeralKind Value: 1; image: 1
Labels: null
Arity: 1
Level: 0
LevelParams: []
LevelConstraints: { }
ArgLevelConstraints: { }
ArgLevelParams: {}
MaxLevel: 2
opLevelCond: [ [ []]]
AllParams: {}
NonLeibnizParams: {}
IsLeibniz: true
isLeibnizArg: true
As can be seen, the null comes from the following construct:
OpApplNode: Operator: $Case - Operands: 3(,,OpApplNode: Operator: $Pair - Operands: 2(null,_))
Unfortunately, the TreeNode representing this semantic node cannot refer to its parents, so there is not obvious way to check the parents of a null operand (to see if it is $Case)> therefore, we have the following ugly fix:
In OpApplNode, we look for the $Case operator and confirm that the third operand is $Pair, then we confirm that the first operands is null. In this case we override the functionality of the xml exporting of these objects. Hopefully, in the future null wont be used as a semantical object
Right now the null node is replaced by:
$Other
After a discussion with Leslie, it occurs to me that one can just export null anytime a node is null and let the reading application (tlapm) figure out what is meant by this null. I have already implemented the above solution but Martin and Leslie should decide together how they want to proceed with regard to both nullpointer errors.
In many cases with concurrency, it occurs that some states can be reached by more than one predecessor states. The trace graph is important in recovering/debugging or analysis. So it's urgent to enhance the trace persistency.
java.lang.ArrayIndexOutOfBoundsException: 0 at tla2sany.semantic.OpDefNode.getMaxLevel(OpDefNode.java:1074) at tla2sany.semantic.Subst.getSubLCSet(Subst.java:147) at tla2sany.semantic.SubstInNode.levelCheck(SubstInNode.java:419) at tla2sany.semantic.OpDefNode.levelCheck(OpDefNode.java:930) at tla2sany.semantic.ModuleNode.levelCheck(ModuleNode.java:850) at tla2sany.drivers.SANY.frontEndSemanticAnalysis(SANY.java:314) at ...
The zip file Linearizability.zip contains two specs that produce the error though cause different stack traces.
@ahelwer: "I installed 1.5.3, and on a fairly complicated spec it does not display the error trace in the GUI:
Double-clicking those states does nothing and provides no further details. Weirdly, if I look inside MC.out I see the state trace just fine:
@!@!@startmsg 2110:1 @!@!@
Invariant inv_149384363400123000 is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@startmsg 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@startmsg 2217:4 @!@!@
1:
/\ IsNodeUp = (n1 :> TRUE @@ n2 :> TRUE @@ n3 :> TRUE)
/\ NetworkPath = ( <<n1, n1>> :> TRUE @@
<<n1, n2>> :> TRUE @@
<<n1, n3>> :> TRUE @@
<<n2, n1>> :> TRUE @@
<<n2, n2>> :> TRUE @@
<<n2, n3>> :> TRUE @@
<<n3, n1>> :> TRUE @@
<<n3, n2>> :> TRUE @@
<<n3, n3>> :> TRUE )
/\ LockTimeout = FALSE
/\ BackupLock = None
/\ IsTakingBackup = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE)
/\ Leader = None
@!@!@ENDMSG 2217 @!@!@
@!@!@startmsg 2217:4 @!@!@
2: <Action line 138, col 24 to line 138, col 37 of module NodeBackup>
/\ IsNodeUp = (n1 :> TRUE @@ n2 :> TRUE @@ n3 :> TRUE)
/\ NetworkPath = ( <<n1, n1>> :> TRUE @@
<<n1, n2>> :> TRUE @@
<<n1, n3>> :> TRUE @@
<<n2, n1>> :> TRUE @@
<<n2, n2>> :> TRUE @@
<<n2, n3>> :> TRUE @@
<<n3, n1>> :> TRUE @@
<<n3, n2>> :> TRUE @@
<<n3, n3>> :> TRUE )
/\ LockTimeout = FALSE
/\ BackupLock = None
/\ IsTakingBackup = (n1 :> FALSE @@ n2 :> FALSE @@ n3 :> FALSE)
/\ Leader = n1
@!@!@ENDMSG 2217 @!@!@
(and so on)
It just doesn't appear to make its way into the error trace in the GUI.
"
TLC module overrides do not work with cloud TLC. The corresponding .class (and .java) files are not include in the jar package that is sent to the cloud instance.
See https://github.com/tlaplus/tlaplus/blob/770a070649e89e21487ffeea3fab50e02bcfff32/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/PayloadHelper.java to include the files in the jar package.
java tlc2.TLC /Users/xxx/HourClock.tla is not supported. Instead, users require to copy these files to the current dir.
The path of .cfg and .tla is processed in two ways. cfg path is processed by the raw path by input. tla path is processed by the filename after discarding the dir info, which is not used in the construction of the spec object. The same action for the two is that find corresponding resource by the preprocessed path in the current dir and the builtin dir(bin/tla2sany/StandardModules).
So the least effort for me temporarily is copying the HourClock.tla and HourClock.cfg into the current dir(tlaplus), then i can run it in eclipse or by command.
Maybe the following snippet will help you.
// cfg path
// function parse(), ModelConfig.java
FileInputStream fis = FileUtil.newFIS(resolver.resolve(this.configFileName, false));// tla path
// function frontEndParse(SpecObj spec, PrintStream syserr), SANY.java
if (!spec.loadSpec(spec.getFileName(), spec.parseErrors)) 
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.