Error with safe strategy synthesis in cruise control example

[magoorden]

Describe the bug I tried to run the queries from the cruise control example (cruise.xml), and I noticed that Stratego failed to synthesize a safe strategy. I get the following error messages (depending on the beta version):

• Parse error in message from server - Expected "START_OBJECT", got "EOF". (Stratego-8-beta-7)
• Error - Server closed unexpectedly. (Stratego-8-beta-10)

To Reproduce Steps to reproduce the behavior:

1. Open the cruise control example cruise.xml from the demo folder.
2. (Necessary in beta 10) Delete the __RESET__ location from Monitor.
3. Go to the Verifier tab.
4. Run the query strategy safe = control: A[] distance > 5.
5. Wait for the error.

Expected behavior No error, or a more user-friendly description of what is wrong with the model.

Version(s) of UPPAAL tested Tested with Uppaal Stratego 8 beta 7 and beta 10.

Desktop (please complete the following information):

• Version UPPAAL 4.1.20-stratego-8-beta7 (rev. A794F860A0933DC4), April 2021.
• Version UPPAAL 4.1.20-stratego-8-beta10 (rev. 383B2943ABF5B142), September 2021.
• OS, Java version: Ubuntu 20.04.2 LTS

[magoorden]

Problem is no longer present in beta 11.

[magoorden]

Well, in beta 11 the error is now thrown inconsistently. After installing beta 11, synthesizing a safe strategy went fine. But after calling the query a couple of times, I now get Error - Server closed unexpectedly a couple of times. Restarting Stratego does not always solves the problem.

[magoorden]

I did some more experiments to see what I need to do to replicate the error. The problem could be related to memory issues.

I'm running Uppaal Stratego in a virtual Linux environment on my MacBook. This virtual Linux environment has a preset base memory, which might be insufficient for running the safe synthesis query. Two indications that it could be a memory issue:

• Once I encounter the error, closing and restarting Uppaal Stratego did not solve the problem. I had to restart the complete virtual machine to resolve the problem (temporarily).
• Monitoring the memory usage with top I can see that the free memory goes down to about 100 MiB just before Uppaal Stratego stops and throuws the error.

In case it is indeed a memory issue, the error message should be more user friendly. Now I had the impression that something was wrong with Uppaal Stratego, while in case of an out-of-memory issue, nothing is wrong with the tool

[yrke]

We expect this issue should be fixed in latest preview release UPPAAL 4.1.20-stratego-8-beta12. (Beta 12 however does not include the concrete simulator)

[RasmusRendal]

This issue seems to have been solved in stratego 9.