This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 670

Summary: Bug: Ok expected
Product: UPPAAL Stratego Reporter: Frederik Baymler Mathiesen <fmathi16>
Component: GUIAssignee: Marius Mikučionis <marius>
Status: RESOLVED DUPLICATE    
Severity: normal    
Priority: P5    
Version: unspecified   
Hardware: PC   
OS: Linux   
Architecture: x86_64 (64bit)

Description Frederik Baymler Mathiesen 2019-10-16 09:21:51 CEST
In version 4.1.20-6 of UPPAAL Stratego, when you choose a diagnostic trace of any kind (some, shortest, fastest), you get a prompt with "Bug: Ok expected".

The terminal shows the following stacktrace:

Bug: Ok expected
	at com.uppaal.engine.Parser.parseProlog(Parser.java:54)
	at com.uppaal.engine.Parser.parseConcreteSuccessor(Parser.java:906)
	at com.uppaal.engine.DotProtocol.getConcreteSuccessor(DotProtocol.java:92)
	at com.uppaal.engine.protocol.JsonProtocol.getConcreteSuccessor(JsonProtocol.java:321)
	at com.uppaal.engine.EngineStub.getConcreteSuccessor(EngineStub.java:633)
	at com.uppaal.engine.Engine.getConcreteSuccessor(Engine.java:317)
	at on.fU.run(Unknown Source)
Comment 1 Marius Mikučionis 2019-10-16 10:16:43 CEST
I am not sure what query your are trying, but I suspect that it is an SMC query and the reason for this bug is that engine returns a concrete trace but the concrete simulator is broken and thus crash. 
We are currently working on the concrete simulator.

If the query is a simbolic one (A[], E<> etc), then this is new, and I would like more details (please confirm).
Comment 2 Frederik Baymler Mathiesen 2019-10-16 11:02:14 CEST
You are right. The problem only occurs for SMC queries.

*** This bug has been marked as a duplicate of bug 643 ***