Describe the bug
I noticed today that changing the parameter Discretization step for hybrid systems only took effect after reloading the model with Reload Simulator. This feels counter-intuitive (at least it is not explained that you have to do this), but maybe necessary as the options are now saved in the model.

To Reproduce
I have created a MWE: MWE_changeoptions.xml.zip.
Steps to reproduce the behavior:

1. Open de MWE.
2. Go to Verifier tab, run the simulate query, and open the plot of the results. I should look like a smooth curve going from 40 to 0.
3. Go to Options -> Statistical parameters, change the value for Discretization step for hybrid systems to 1.0, and click OK to close the option window.
4. Run the simulate query again and open the plot of the results. The plot should look suspiciously the same.
5. Reload the model to the server by pressing F5 or going to View -> Reload Simulator.
6. Run the simulate query again and open the plot of the results. Now you see that curve no longer goes to 0 (it is flat around 18).
7. (Optionally) Go to Options -> Clear option overrides. Now perform steps 4-6 again so see that the change only happens after reloading the model.

Expected behavior
After changing options for the queries, the changed options should have immediate effect when queries are run again. Maybe changing settings should automatically reload the simulator.

Version(s) of UPPAAL tested
UPPAAL Stratego 8 beta 7.

Desktop (please complete the following information):

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

Additional context
Problem is also present if options are changed for queries individually with the clockwheel button.

Is your feature request related to a problem? Please describe.
I use XTA file format since it is easier to edit in text editor, works better in git and unlike the XML format, it does not mix presentation with code. When I add a comment to an edge, it is stored as a multi-line documentation comment on a line above the edge. Unfortunately, it is ignored when the file is opened in UPPAAL and so it gets removed on saving.

Describe the solution you'd like
The parser should preserve documentation comments before language features that can be commented in the interface. That is what various documentation generators do.

Describe alternatives you've considered

• I could use the XML format but that is less nice for editing in a text editor.
• I could add the following conjunct to the guard: "comment" != "" that is a syntax error.

Describe the bug
When using the buildin function fint(), it is not possible to use the simulator anymore because we get the error "Server connection lost"

To Reproduce
Steps to reproduce the behavior:

1. Create a template
2. Add a transition with as update the call of the function cast()
3. In the declarations of the template define:
   int x=0;
   double dx=0.0;
   void cast() { x = fint(dx); }
4. Do not forget to declare the system in the system declaration
5. Open the simulator tab and see the error

Expected behavior
When clicking the simulator tab, no error should appear and I should be able to execute my simulation.

Desktop:

• OS: Ubuntu 18.04.5 LTS
• Version Uppaal 4.1.24 (rev. 29A3ECA4E5FB0808), November 2019

Describe the bug
UPPAAL 4.1.24 (rev. 29A3ECA4E5FB0808) and UPPAAL 4.1.20-stratego-7 (rev. 12D93ED5FE521036), clicking the uppaal.exe shows:

However, when running: java -jar uppaal.jar in the command line, they start correctly.

In addition, running UPPAAL65-4.1.25-5 in the command line: java -jar uppaal.jar, it shows:

Error: A JNI error has occurred, please check your installation and try again
Exception in thread "main" java.lang.UnsupportedClassVersionError: com/uppaal/gui/Main has been compiled by a more recent version of the Java Runtime (class file version 55.0), this version of the Java Runtime only recognizes class file versions up to 52.0
at java.lang.ClassLoader.defineClass1(Native Method)
at java.lang.ClassLoader.defineClass(ClassLoader.java:756)
at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
at java.net.URLClassLoader.defineClass(URLClassLoader.java:468)
at java.net.URLClassLoader.access$100(URLClassLoader.java:74)
at java.net.URLClassLoader$1.run(URLClassLoader.java:369)
at java.net.URLClassLoader$1.run(URLClassLoader.java:363)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:362)
at java.lang.ClassLoader.loadClass(ClassLoader.java:418)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:352)
at java.lang.ClassLoader.loadClass(ClassLoader.java:351)
at sun.launcher.LauncherHelper.checkAndLoadMain(LauncherHelper.java:601)

Version(s) of UPPAAL tested
(Academic) UPPAAL 4.1.24 (rev. 29A3ECA4E5FB0808), November 2019
(Academic) UPPAAL 4.1.20-stratego-7 (rev. 12D93ED5FE521036), December 2019
(Academic) UPPAAL 4.1.25-5 (rev. 643E9477AA51E17F), April 2021

Desktop (please complete the following information):

• My OS: Edition Windows 10 Education
  Version 21H1
  Installed on ‎1/‎13/‎2021
  OS build 19043.1052
  Experience Windows Feature Experience Pack 120.2212.2020.0

• My version of JAVA:
  openjdk version "1.8.0_292"
  OpenJDK Runtime Environment (AdoptOpenJDK)(build 1.8.0_292-b10)
  OpenJDK 64-Bit Server VM (AdoptOpenJDK)(build 25.292-b10, mixed mode)

Describe the bug
When you try to use a derivative in the simulate query, the reported error is "Integer or clock expected". This error message is incorrect, as e.g. doubles are also allowed (and possibly other variable types).

To Reproduce
Follow these steps to reproduce the problem:

1. Have a valid model with a clock variable (for example clock x) and a double variable (for example `double y').
2. Go to the Verifier tab and create a simulate query using the derivative of the clock, for example simulate 1 [<=10] {x'}
3. Run the query and observe the error message.
4. In the query, replace the clock derivative by the double variable, for example simulate 1 [<=10] {y}
5. Run the query again and observe that the same error message does not appear.

Expected behavior
The error message should state all the allowed variable types.

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

Desktop (please complete the following information):

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

Describe the bug
When a model calls external libraries (.dll/.so) in UPPAAL STRATEGO, if parameters of the functions are data structs, some of their values are wrong when they are received in the C space. According to my observation, if one prints the parameters in the C space, he/she would see the first two elements in the data struct are usually correct, but the rest is wrong.

To Reproduce
Steps to reproduce the behavior:

1. Write a DLL in Windows, or a SO in Linux, where a function that has at least a parameter whose type is a data struct prints its parameters;
2. Import the DLL/SO in UPPAAL STRATEGO;
3. Write a property that would surely go to the transition where the external library is called;
4. Run "verifyta" by command line.

Expected behavior
In the command line, the printed parameters should have the same value that you passed to them. But some of them have surprisingly big values.

Desktop (please complete the following information):

• OS: Windows 10

These are questions and suggestions from AMOST/ICST invited tutorial on April 12, 2021

• I would like to simulate a particular behavior sequence in the simulator and then use it as a test case
  • The test generator tab should be able to import the trace from the simulator
• Explain how to create a test case which exercises the same feature several time (e.g. "failed to connect twice"). Documentation should explain that it can be achieved by using purpose/query-based test case generation where:
  • The model has a counter associated with the feature (e.g. increment a counter when the connection failed)
  • Or use observer automaton to monitor a specific sequence of events.
• It would be nice to be able to compose several test cases sequentially. Two solutions:
  • An observer automaton can be used to guide the model-checker to achieve specific sub-goals.
  • The model.jar API allows model-checking queries from a specific state, thus the GUI needs to be extended to facilitate trace extensions.

Describe the bug
Clock guards on broadcast receivers do not give an error or the "correct" transitions.

To Reproduce
broadcastreceiverguard.xml.gz

Make two new templates (Sender and Receiver) and a global clock and a broadcast channel.

Have the Sender send within the interval [0, 3] and have Receiver can har guard for x == 1. Instantiate these two templates.

Expected behavior
Either

• an error telling me that I cannot have clock guards on the edge with broadcast receive,
• or enter the symbolic model checker tab and see 3 transitions.
  • [0, 1) with no receivers.
  • [1, 1] with one receiver.
  • (1, 3] with no receivers.

Currently there are 2 identical transitions for [0,1), 1 transition for x = 1, and 1 deadlock state when x>1.

Version(s) of UPPAAL tested
I have tried with stratego-8-beta7.

Copyright (c) 1995 - 2021, Uppsala University and Aalborg University.
All rights reserved.
Compiled with g++-10 -Wall -Wempty-body -DNDEBUG -O3 -ffloat-store -fPIC -mtune=generc -DLIBXML_STATIC -DENABLE_TIGA -DMULTI_TERMINAL -DENABLE_TIGA_SMC -DENABLE_TIGA -DMUTI_TERMINAL -DENABLE_STORE_MINGRAPH -DTIGA_OTF_BUCHI -DENABLE_LSC -DENABLE_POLYHEDRA_HECKING  -DBOOST_DISABLE_THREADS -std=c++17
Free for academic and non-commercial use only.

Desktop (please complete the following information):

• Version [see Help About menu, or verifyta --version e.g. 4.1.25]
• Kubuntu 20.10, 64 bit

Describe the bug
Verification does not terminate gracefully and keeps computing in the background

To Reproduce
Steps to reproduce the behavior:

1. load a model
2. go to verifier
3. check a property which takes significant time
4. click cancel
5. observe that the verification dialog is gone, but the engine is still using CPU

Expected behavior
When the verification dialog disappears, engine stops computing and keeps the previously results (e.g. strategies) intact.

Consider declaration:

clock u;
double funcu() {  return u; } 
double funcu0() { return u + 0; }

Then query simulate [<=4; 1] { funcu(), funcu0() } results in the following plot:

which shows unexpected trajectory of funcu(), where the expectation is that it should coinside with funcu0.

Tested on Uppaal-4.1.24,

Meanwhile Uppaal Stratego 4.1.20-7 shows a different, also unexpected, plot:

Uppaal Stratego on the main branch:

Reported by Ulrik Nyman.

Describe the bug
If a modeler changes the model in the Editor tab and subsequently wants to run an existing query, the GUI is detecting that the model in the Editor tab differs from the one currently in use by the server. It generates a pop-up window and asks the user whether it should upload the new model to the server. Answering with Yes generates an error (often I get "Parse error in message from server: Expected "START_OBJECT", got "EOF"", sometimes also "Positions must be monotonically increasing"; subsequent tries can also generate memory issue errors.) Manually reloading the model to the server does solve the problem.

To Reproduce
The MWE from my previous bug report #44 can also be used here. I assume the problem can be reproduced with any model.
Steps to reproduce the behavior:

1. Open the MWE.
2. Go to the Verifier tab and run the simulate query (just to make sure the current model is properly uploaded to the server).
3. Go to the Editor tab and change something in the model. For example, the initial value of w can be changed from 40.0 to 50.0.
4. Go back to the Verifier tab and try to run the query again.
5. Click Yes in the pop-up window on whether to upload the new model to the server.
6. Get the error.

To get the memory issues, continue with the following steps:
7. Click OK to close the error window.
8. Try to run the query again. Now you should get a "Stream closed" error.
9. Manually reload the model to the server.
10. Run the query again to observe now there is no problem.
11. Go to the Editor tab and change the model again. For example, change the initial value of w back to 40.0.
12. Go to the Verifier tab and run the query.
13. The followin error message is displayed "Memory exhausted. See
http://bugsy.grid.aau.dk/bugzilla3/show_bug.cgi?id=63
for more information."

Expected behavior
When the user selects Yes to upload the modified model, there should be now errors (only in case the changes to the model justify returning an error to the user).

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

Desktop (please complete the following information):

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

Describe the bug
In Stratego-8-beta-6, options other than the default ones can be saved for each query specific. For some of the options, opening such a model result in an internal error "Caught unexpected java.lang.RuntimeException: Could not interpret parameter field properly." At least one of the options resulting in this error is Number of successful runs. At least one of the options resulting in no error is Discretization step for hybrid systems. I don't exhaustively tested all options to figure out which of them result in this internal error.

To Reproduce
Steps to reproduce the behavior:

1. Have a Uppaal model without saved settings.
2. Select a query.
3. Click the gear button.
4. Go to Learning parameters
5. In the pop-up window, change `Number of successful runs' (the first option) to something else, for example 20 (removing the last 0). A red star should appear behind the option name.
6. Click OK. Verify that the gear button now has a small yellow circle.
7. Save the file. You might want to verify that the option has been saved by looking in the xml file for the <option/> tag.
8. Open another (random) Uppaal model.
9. Open the Uppaal model with the saved option.
10. Internal error appears.

Expected behavior
No internal error while opening the model. Expected behavior can be observed by following the steps above, but now changing the Discretization step for hybrid systems option.

Uppaal version

• Uppaal Stratego 8 beta 6.

Desktop (please complete the following information):

• OS: Ubuntu 20.04.1 LTS.

Describe the bug
In Stratego-8-beta-6, non-default options are saved together with the queries. Unfortunately, opening a model with such saved non-default settings does not import these settings into Uppaal. To be precies, this concerns the options that hold for all queries, i.e., those changed through the Options menu in the top of the GUI. Loading options goes fine when they are saved for a specific query by using the gear button next to the query field.

To Reproduce
Steps to reproduce the behavior:

1. Have a Uppaal model with non-default settings saved. This can be verified by looking for the <option/> tag in the xml file.
2. Open the model in Uppaal.
3. In options, the default values are shown and not the values in the model file.
4. Running queries use the values shown in the option drop-down menu and not the options saved in the model file.

I have tested this for a limited set of options (discretization step for hybrid systems, number of succesful runs, maximum number of runs, number of good runs, and number of runs to evalue).

Expected behavior
When a model is opened with saved settings, the option drop-down menu should reflect this and queries should used the saved option settings.

Uppaal version

• Uppaal Stratego 8 beta 6

Desktop (please complete the following information):

• OS: Ubuntu 20.04.1 LTS.

Describe the bug
The Learning Parameter fields throw exceptions if one changes values that include a comma.

To Reproduce
Steps to reproduce the behavior:

1. Go to Options -> Learning Parameters
2. Change the first parameter to 1000 and chose any other field. (The UI will change the value to "1,000" with a comma)
3. Now go back to the first parameter, click after the last digit and remove it.
4. The field now has the value "1,00", and an exception is thrown.

Expected behavior
Remove the comma to show the value "100".

Version(s) of UPPAAL tested
UPPAAL 4.1.20-stratego-8-beta7 (rev. A794F860A0933DC4)

Screenshots

Desktop (please complete the following information):

• Ubuntu 20.10, Java openjdk 14.0.2 2020-07-14

the zoom tools should increase the font of the query list and editor widgets

Describe the bug
The About window refers users to the old Bugzilla issue tracking system.

Expected behavior
The About window should refer users to Github for reporting issues.

Version(s) of UPPAAL tested
UPPAAL Stratego-8-beta-7

Desktop:

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

Is your feature request related to a problem? Please describe.
Some natural feeling declarations are currently not accepted related to the initialization of variables. It gives the user the error message "Must be computable at compile time". An example is the following declaration of two integer variables:

int i = 0;
int j = i;

From a modeling perspective, the variable i is initialized to the value 0, and the variable j to the value of i, which is 0 at initialization.

The documentation does not help the modeler in understanding what the error message means. There is nothing on computable, and the grammar for a declaration simply states that Initialiser ::= Expression | '{' Initialiser (',' Initialiser)* '}'.

Describe the solution you'd like
The desired solution would be to accept the model.

Describe alternatives you've considered
The problem can be circumvented by introducing another constant variable and using that for the initialization of other variables. For the example, the workaround is

const int init = 0;
int i = init;
int j = init;

The downside is that the model will contain more variables to understand and maintain, as you need to introduce a constant for each specific initial value (for example, if initial value of j is i + 1, you would already need to introduce two constants). This can become problematic especially when the model contains arrays.

The attached model (clock_prob_weight.xml) reports that the sum of probabilities are <=0 which is wrong.
The expected outcome should be as in clock_prob_weight_fint.xml, specifically:

Pr[<=100] (<> Process.LX) is 2/3 and
Pr[<=100] (<> Process.LX) is 1/3

clock_prob_weight_models.zip

Describe the bug
If you have a new unsaved system and you want to save it, Uppaal normally detects that the location where to save the system has not been specified and asks the user to name the file before it actually saves it. In some particular cases, Uppaal fails to correctly identify a new system as a new system, and thus when saving it 'for the first time', it overrides the previously opened model. In this way, I lost a MWE for another bug report.

To Reproduce
Steps to reproduce the behavior:

1. Freshly open Uppaal and create a new model. For example, you can define in the global declarations a clock x with clock x = 0.0;.
2. Save the new system by clicking on the save button.
3. Uppaal asks how the system should be saved in a pop-up window. Save it with your favorite name, for example test.xml.
4. Change the model in some way, but do not save it yet. For example, you can change the initial value of clock x to 1.0.
5. Click on the button to create a new system.
6. Uppaal will ask you now to save the current system before the new one is created. Click save. (I haven't checked what happens if you click don't save or cancel.)
7. A new system is opened for you. Notice already in the top bar of Uppaal that this new system has the same name as the previous one. So in my example it still shows test.xml - UPPAAL. This is a first sign that something is about to go wrong, but user (me included) miss this for the first time.
8. Put something else in the global declaration, like clock y = 10.0;, or leave it as it is by default.
9. Save the new system by clicking the save button.
10. Notice that Uppaal does not ask this time how the new system should be save. Thus you just have overwritten your previous save.
11. Verify that the first model as created in step 1 is lost and the file only contains the latest model as created in step 8.

Expected behavior
At step 7 above, everything should be labeled as new system. So once this new system is being saved for the first time, Uppaal correctly asks the user how the new save should be called.

Version(s) of UPPAAL tested
Tested with UPPAAL v4.0.15 (the current official stable release) and UPPAAL Stratego 7 beta 8 (the latest one I have).

Desktop (please complete the following information):

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

Describe the bug
In the attached model it is not possible in the concrete simulator to take the transition with off! It is possible in the symbolic simulator.
lightswitch.xml.zip

To Reproduce

1. Open attached model
2. Open the concrete simulator
3. Take the enabled transition
4. It should now be possible to take the transition with the off! sync but it is not possible.

Expected behavior
It should be possible to take the transition in the concrete simulator

Desktop (please complete the following information):

• OS: Manjaro Linux
• Version: Stratego-8-beta-6

Is your feature request related to a problem? Please describe.
Currently in Uppaal Stratego, derivatives of clock values are not observable in simulate queries (and possible other queries as well). If you try to use a clock derivatie in the simulate query, you get the error "Integer or clock expected" (which is, btw, an incorrect statement, see #48).

Consider a model with clock variable x and a location invariant describing its derivative as x' = some_function() where some_function() is a user-defined function. In validating the model, the simulate query can be used to observe the behavior of x. But in case the behavior is counter-intuitive, further investigation can benefit from also displaying the values from x' or `some_function()' directly.

Describe the solution you'd like
Clock derivatives should be allowed in the syntax of (some specific) queries.

Describe alternatives you've considered
A workaround is to explicitly create a reporting mechanism. For example:

Declare in the same template as x a double der = 0.0, const double P = 1.0, and clock p, where der is the variable storing the value of the derivative, P is the reporting interval (which of course can have different values, but a user should keep the option value for 'Discretization step for hybrid systems' in mind), and p the clock keeping track of the reporting intervals.
Add to the location with the derivative of x an uncontrollable selfloop labeld with guard p == P and update der = some_function(), p = 0. Also add to the same location the invariant p <= P.
Now the variable der can be used in the simulate query to obtain the value of x' once every period P.

In some rare cases, the reported value can be different from the actual value of x'. Consider the case that once p==P holds, also somewhere else in the model a transition is enabled and the effect of that transition changes the value of some_function(). Now the order of dealing with stuff in the simulation might be that we first do the reporting selfloop, then the other transition, and then the calculation of x'. In this case, 'der != x'`.

Dear all,
the official documentation at

https://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Declarations.shtml

also provides this example

==================
The following declares a record type S containing an integer a, a boolean b and a clock c:

typedef struct
{
int a;
bool b;
clock c;
} S;

however, such struct results in an error "Invalid type in structure" in Uppaal.

Best
Davide

Describe the bug
Consider a model with a user-defined function using if-else statements. Plotting this function with the simulate query results in an incorrect graph. In the simple MWE included below, the plotting functionality only shows the result of the first if-statement, without switching to the else statement at appropriate times.

To Reproduce
This MWE can be used to illustrate the problem. It contains two user-defined functions were w is a clock going from 100 to 0 in 10 seconds:

double direct()
{
    return trunc(w);
}

double indirect()
{
    if (w <= 0) return 0;
    else return trunc(w);
}

Steps to reproduce the behavior:

1. Go to the Verifier tab.
2. Check the simulate query.
3. Open the graph.
4. See that the plot of indirect() is not the same as direct().

You can also change the return value of the if statement in indirect() to other values, like 10, and see that the plot of this function changes to the value you just inserted.

Expected behavior
The plot should correctly follow the cases as defined in the if-else statements. So in the MWE, the plots of direct() and indirect() should be exactly the same for the time interval [0,10].

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

Desktop (please complete the following information):

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

Describe the bug
Probability Density Distribution graph cut's off the leftmost digit.

To Reproduce
Steps to reproduce the behavior:

Model: error_cut.tar.gz

1. Execute Uppaal-XML with set learning parameters (Might not be important with these settings, but it gives a strategy faster):
   • Number of successful runs: 1000
   • Maximum number of runs: 1000
   • Number of good runs: 1000
   • Total maximum number of iterations: 1
   • m_option_imitation_iterations: 1
2. Execute the probability query.
3. On the second query, right-click and choose Probability Density Distribution. Here the leftmost digit is cut away.

Expected behavior
The leftmost bucket should start at 270, not just 70. Especially when the displayed samples are in [276.7, 1830]

Version(s) of UPPAAL tested
UPPAAL 4.1.20-stratego-8-beta7 (rev. A794F860A0933DC4)

Screenshots

Desktop (please complete the following information):

• Ubuntu 20.10, Java openjdk 14.0.2 2020-07-14

We do not have much guidance on how to structure the variables, but currently the trend is to put as many variables as possible into local scopes (structs and templates), even declare them in the system declarations and then share the variables through template parameters.

However there are some limitations:

1. clocks cannot be part of struct
2. doubles cannot be part of struct
3. no recursive function calls (the function cannot be called from inside its body)

so it would be nice to support such structs and allow recursive calls.

Describe the bug
The simulator gives Expected "START_OBJECT", got "EOF" in the simulator after taking the first transition in the attached model:
lightswitch.xml.zip

To Reproduce
Open the attached model, go to simulator, take the only enabled transition

Expected behavior
No exception

Screenshots
If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

• OS: Manjaro linux
• Version: Stratego-8-beta-6

The issue on MacOSX (not reproducible on Linux)

Steps to reproduce:

1. in the menu choose "Template export" -- export dialog pops up
2. select extension JPG
3. click Browse -- a native select file dialog pops up
4. choose some directory (e.g. Documents) and click Save

Result:
Error popup "The file name must have a valid file extension"

Expected:
The export dialog has filled with the path

Details
MacOSX Catalina 10.15.7
Oracle Java 8

I would like to check properties of the form f --> deadlock.

At the moment, Uppaal does not support the use of the dead atomic proposition outside of some very restricted cases.
It would be nice to be able to check formulas such as: f --> deadlock or E[] not deadlock

Describe the bug
Stratego supports hybrid clocks as cost/monitoring variables which work as follows:

1. they are ignored in symbolic analysis (engine builds a symbolic abstraction without the cost/monitoring details)
2. they are reintroduced in concrete analysis (SMC or SMC under symbolic strategy).
   The issue is that updates on hybrid clocks are not allowed, even though such expressions can be ignored in symbolic analysis and reintroduced in SMC queries.

The same treatment can be generalized to floating point variables and their expressions as long as they do not influence the system behavior (do not appear in guards and their value is not read for storage into integer variables).

To Reproduce
Steps to reproduce the behavior:

1. Create a model which represents safe usage, i.e. the following declaration:

clock x;
hybrid clock cost;
double fpcost;

2. Go to verifier and check A[] not deadlock and observe an error telling that the read from hybrid clock and floating point variable is not allowed -- it should succeed and find the (trivial) deadlock.
3. Go to symbolic simulator and observe a similar error -- it should work, except the variables cost and fpcost should not be displayed, just like in symbolic analysis.
4. The concrete simulator should work as expected (fixed on the main branch).

Describe the bug
When a figure is exported to a pdf-file, the resulting file is incomplete where parts are cut off.

To Reproduce
Steps to reproduce the behavior:

1. Generate a plot, for example with the query 'simulate'.
2. Right click on plot area.
3. Select Export > Plot.
4. Safe the figure as a pdf.
5. Open the generated pdf-file to inspect the result.

Expected behavior
The complete figure as shown in UPPAAL.

Screenshots
See the attached example of a generated pdf-file.
Simulations_dynamic.pdf

Desktop:

• OS: Windows10
• Version: UPPAAL 4.1.20-stratego-7

Describe the bug
An infinite loop is triggered if a 2D array value is out of bounds.

To Reproduce
Model: out_of_bounds_2d_array.zip

Steps to reproduce the behavior:

1. Open model out_of_bounds_2d_array.xml.
2. Go into the simulator tab.
3. Wait until the end of time.

Expected behavior
An error that the chosen value is out of bounds.

Version(s) of UPPAAL tested
uppaal64-4.1.20-stratego-8-beta7

Desktop (please complete the following information):

• (Academic) UPPAAL 4.1.20-stratego-8-beta7 (rev. A794F860A0
  933DC4), April 2021
• Ubuntu 20.04.2 LTS, openjdk 11.0.11 2021-04-20

model_and_trace.zip

Describe the bug
-The transition that cannot be enabled (because the corresponding guard is false) is taken so that the corresponding syncronization and update are executed.
-The enabled-taken transition is not displayed in red on the graphical representation in Simulator.

To Reproduce
Steps to reproduce the behavior:

1. Unzip the attached 'model_and_trace.zip' file
2. Open 'SCP_v7.01_3nodes_1quorum_3values(allnodes)_cnt8_gap1_thr100_v4.1.24.xml'
3. In Simulator, open 'SCP_v7.01_3nodes_1quorum_3values(allnodes)_cnt8_gap1_thr100_v4.1.24.xtr' trace file.
4. Proceed to the point where ballotStates[2].curState (in Global variables) becomes 1 from 0' in Simulation Trace. You can find that there are three enabled transitions - 'tickAdvance[0]: NodeTick -> NodeBallot(0)', 'tickAdvance[1]: NodeTick -> NodeNomination(1)', and 'nominationDone[2]: NodeBallot(2) -> NodeNomination(2)'.
5. By pressing Next button, you can see that 'tickAdvance[0]: NodeTick -> NodeBallot(0)' is taken.
6. By pressing Next button, you can see that 'tickAdvance[1]: NodeTick -> NodeNomination(1)' is taken.
7. By pressing Next button, you can find that 'tickAdvance[2]: NodeTick -> NodeNomination(2)' is taken although the guard 'canTick[2] && tickAllowed[2]' along with 'tickAdvance[2]!' is false; thus, cannot be enabled . Moreover, this taken transition is not displayed in red in NodeTick template.

Expected behavior
The only enabled transition 'nominationDone[2]: NodeBallot(2) -> NodeNomination(2)' should be taken.

Screenshots
If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

• OS: Ubuntu 20.04.2 LTS
• Browser: Chromium
• Version: 90.0.4430.72

Describe the bug
The learning-methods of stratego rely on sampling a stochastic system.
Therefor all channels should be marked as broadcast to ensure independent progress, which is required for SMC.

To Reproduce
Attempt to valide the two propositions in the attached model: robot3.zip.
The simulate query will fail with the correct error that "All channels must be broadcast", the following minE proposition computes a strategy but should terminate.

Expected behavior
The verification of the minE property should fail.

Version(s) of UPPAAL tested

• uppaal64-4.1.20-stratego-8-beta8
• newest nightly build: 3E4B8103E3C04E1D

Desktop (please complete the following information):

• OS, Java version: Fedora 33.

Describe the bug
After adding a query for test generation (to existing queries) in the verifier tab, the new query does not show up as option in the Queries portion of the test cases tab. Workaround: quit tool and reload model.

To Reproduce
Steps to reproduce the behavior:
Load model with queries.
go to test cases tab - show query drop down
goto verifyer; add a query
go to test cases tab - show query drop down - the added query is not sho,
Saving model does not help.

Expected behavior
Added query shown

Version(s) of UPPAAL tested
Windows x64 UPPAAL 4.1.25-5

Screenshots
If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

• OS: [e.g. iOS]
• Browser [e.g. chrome, safari]
• Version [e.g. 22]

Additional context
Add any other context about the problem here.

Describe the bug
In beta 6, settings are saved in the underlying xml file. When a user wants to open a new model file, Uppaal checks whether there are changes not saved before actually letting the user load a new model. When unsaved changes are detected, the user is asked whether these changes needs to be saved or not. Unfortunately, this prompt is also shown to the user when changes in settings are already saved.

To Reproduce
Steps to reproduce the behavior:

1. Change a setting trough the Options drop-down menu, for example, set the discretization step for hybrid systems to 1 instead of the default 0.01.
2. Save the model.
3. Verify that the new setting has been saved by opening the xml view of the model (in for example a text editor) and look for the <option/> tag.
4. Request Uppaal to open a system.
5. A 'Save System' prompt is now opened.

Expected behavior
Uppaal should recognize that the changed settings have already been saved.

Uppaal version

• Upaal Stratego version 8 beta 6.

Desktop

• OS: Ubuntu 20.04.1 LTS.

Additional context
The prompt is not shown when settings are reset by pressing Clear option overrides and saving the model before opening another one.

Is your feature request related to a problem? Please describe.
A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
Yes, broadcast causes different answers depending on the operating system

Describe the solution you'd like
A clear and concise description of what you want to happen.
I would like that the user is able to specify and ordering on the receiving edges in a broadcast e.g. bcan?[2], where 2 is a natural number indicating the order. It should be a total order.

Additional context
Add any other context or screenshots about the feature request here.

For the query A<> DriverFast.stable && desired_speed == 78
The following file produces satisfied in Windows and not satisfied in Ubuntu 20.04

sheet2CruiseController_sol.zip

I get the following when I try to start Uppaal:

java.lang.NullPointerException
at on.l.run(Unknown Source)
at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313)
at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:770)
at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
at java.base/java.security.AccessController.doPrivileged(Native Method)
at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:740)
at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

Is your feature request related to a problem? Please describe.
Te UPPAAL verification engine seems to work on traces instead of paths.

Describe the solution you'd like
I would like to be able to specify specific requirements to operate on paths.

Describe alternatives you've considered
An alternative verification engine operating on paths, or perhaps a switch in the settings.

Describe the bug
-Transitions that are not in the Enabled Transitions are taken in Simulator.
-Although Enabled Transitions shows deadlock, many further steps can be added in the simulation trace.

To Reproduce
Steps to reproduce the behavior:

1. Unzip the attached 'model_and_trace2.zip' file
   model_and_trace2.zip
2. Open 'SCP_v8.01_3nodes_1quorum_3values(allnodes)_cnt8_gap1_thr100_v4.1.24.xml'
3. Go to Simulator, open the trace file ‘SCP_v8.01_3nodes_1quorum_3values(allnodes)_cnt8_gap1_thr100_v4.1.24.xtr'.
4. Proceed to the point where ballotStates[2].curState (in Global variables) becomes 1 from 0' in Simulation Trace. You can find that there are three enabled transitions - 'NodeNomination(1)’,’NodeBallot(0)', and ‘nominationDone[2]: NodeBallot(2) → NodeNomination(2)’
5. By pressing Next button, you can see that 'NodeNomination(1)' is taken.
6. By pressing Next button, you can find that 'NodeNomination(2)' is taken and update is done although it is not in the Enabled Transition. Moreover, this taken transition is not displayed in red in NodeNomination(2) template.
7. By pressing Next button, ’NodeBallot(0)' in Enabled Transitions is taken.
8. By pressing Next button, ’NodeNomination(0)' in Enabled Transitions is taken.
9. By pressing Next button, ’NodeBallot(1)' in Enabled Transitions is taken.
10. By pressing Next button, you can find that ‘nominationDone[2]: NodeBallot(2) → NodeNomination(2)’ in Enabled Transitions is not taken and another transition of NodeBallot(2) is taken which is enabled by the undesired execution described in Step 6. A This taken transition is not displayed in red in NodeBallot (2) template.
11. At the latter part of the trace, you can find ‘deadlock’. Although Enabled Transitions shows deadlock, many further steps can proceed in the simulation trace. Suddenly NodeSlot(0) moves from SlotStarted to SlotUnknown in the last step, although the guard is not true.

Expected behavior
-'NodeNomination(2)' shouldn’t be taken because it is not in the Enabled Transition.
-The only enabled transition 'nominationDone[2]: NodeBallot(2) -> NodeNomination(2)' should be taken.

Version(s) of UPPAAL tested
UPPAAL v4.1.24

Screenshots
If applicable, add screenshots to help explain your problem.

Desktop (please complete the following information):

• Version: UPPAAL 4.1.24
• OS: Ubuntu 20.04.2 LTS

Additional context
Add any other context about the problem here.

Is your feature request related to a problem? Please describe.
I cannot see both Message Sequence Chart and Processes at the same time on my display.

Describe the solution you'd like
It would be nice if the MSC was detachable like Variables and Simulation Control is so I could move it to another display.

Describe alternatives you've considered

• I could expand the MSC manually but it is inconvenient and does not allow viewing both at the same time.
• I could arrange my screens vertically and resize the window so it covers both of them but my secondary screen is narrower so I would have to sacrifice some width of the Processes
• I could buy a larger screen but FullHD should be more than enough.

Describe the bug
Assigning an out-of-range value to typedef'ed valuetype gives an XML error in the GUI, but the verifier gives a correct answer.

In the simulator tab, the error Expected field name "src", got "path" is given.

To Reproduce
Steps to reproduce the behavior:
1.Get the model out_ot_range_assignment.xml from here:
out_of_range_assignment.zip
2. Go to the Simulator tab.
3. See error.

Expected behavior
The same error message as when the query in the Verifier tab is run.

Notes
Error messages workes fine for Concrete Simulator & Verifier,

Version(s) of UPPAAL tested
4.1.20-stratego-8-beta7, 4.1.20-stratego-8-beta8, 4.1.20-stratego-8-beta9, 4.1.20-stratego-8-beta11

Desktop (please complete the following information):

• (Academic) UPPAAL 4.1.20-stratego-8-beta7 (rev. A794F860A0
  933DC4), April 2021
• Ubuntu 20.04.2 LTS, openjdk 11.0.11 2021-04-20

This report is about many issues which need to be addressed systematically (preferably all at once).

Currently Uppaal always implements signed int32_t operations, which might be incorrect when overflows happen.
In general Uppaal always checks the ranges and does not allow overflows (reports an error), but:

1. often embedded system allow overflows, thus such range-checking can get in the way. Perhaps we can introduce "relaxed int" type without range checking (this is not critical, thus fixing this has low priority).

2. Uppaal fails to detect when int32_t overflow happen. Perhaps Uppaal should use int64_t operations and check for 32bit overflow. In assembly it is possible to check the Carry flag and thus the operation could still be over int32_t and cheaper.

3. It is not possible specify uint32_t range:
   Parser does not allow large integer constants like 4294967295. A workaround 2147483647 << 1 +1 works, but gets interpreted as negative value and thus the type declaration fails. Even if the type system is fixed, we still need to revise the integer operations in the virtual machine.

4. Uppaal does not implement bitwise negation. The reason is that the size of our ranged integers is not specified (not sure how many and which bits need to be flipped, especially in case of a sign bit). C/C++ define the bitwise operations over unsigned integer types, so perhaps the easiest solution would be to promote to the full size (uint32_t), but this is not possible because of the second issue, moreover it is not clear how the mixed arithmetic (between signed and unsigned types) works (C/C++ have rules, but Uppaal just treats everything as int32_t).

5. int32_t etc should be built-in types, along with INT32_MAX and other constants.

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

Describe the bug
When symbolic methods fail due to unsatisfied prerequisits, the message "v gameInfoCounterPlay" is shown to the user in a popup window, which apparently should indicate that there is an opponent strategy disproving the existence of a winning strategy. This is a misleading message. The user will only realize that there is an error when the user has the Status visible at the bottom of the Query tab, where the actual error message is shown, or when the user goes to the Editor tab, where the actual error is shown in the issue list at the bottom.

To Reproduce
Steps to reproduce the behavior:

1. Open the attached model with a minimal working example.
2. Run the query.
3. See popup window with message, and observe that the grey circle is still grey.
4. Make the Status subwindow large enough to see the error message or switch back to the Editor tab to see the actual problem.

Expected behavior
The popup window should clearly indicate that the model does not satisfy the prerequisits for the query and that the user should go back to the Editor tab to see the complete list of issues.

Desktop

• OS: Ubuntu 20.04.2 LTS
• Stratego version: issue observed in Stratego-7 and Stratego-8-beta-6

Additional comment
Smaller end-user issue: the message "v gameInfoCounterPlay" is not clear for an end user. The user needs to consult documentation (in my case asking Peter) to decrypt it.

MWE_SynthesisStatus.zip

Describe the bug
Simulator crashes on a guard of the following form:

forall(i:id_t)
  x[i]<5 && cond[i]

where:

const int N = 3;
typedef int[0,N-1] id_t;
bool cond[id_t] = { 1,1,1 };
clock x[id_t];

To Reproduce
Steps to reproduce the behavior:

1. Load the model
2. Go to simulator
3. Execute one transition
4. Observe engine crash

Expected behavior
It should just execute further.

Screenshots

Additional context
The issue is with method DiscreteState::hasUrgentEdge() which creates only the discrete-state evaluation context and thus clock-guard evaluation part crashes.

Original report: https://bugsy.grid.aau.dk/bugzilla/show_bug.cgi?id=681

Describe the bug
Squaring a variable by multiply it by itself x * x is much faster than using pow(x, 2) function.

To Reproduce

Global declaration

clock Cost;

Templates
objective

objective_pow

Verifier - objective

system objective;

Pressed F5 to reload

Verifier - objective_pow

system objective_pow;

Expected behavior
Expected for both to take similar time to be interchangeable when defining expressions

Desktop

• OS: Ubuntu 20.04.2 LTS
• UPPAAL 4.1.20-stratego-8-beta6 (rev. 2B32AEEE2ECD4B4F), January 2020

DLL feature requires a low level C programming experience and deep understanding how the DLLs work in general.
In addition, the DLL interface suffers from DLL-hell where all the libraries must be compiled against the compatible C-library.

I propose to provide a handful of generic libraries for simple lookup using CSV files, which would serve both as an example implementation and a quick trajectory/dictionary import from CSV files. The libraries can also be precompiled and shipped with the distribution, so the user can use them straight away.

Currently, there is no way to pass strings to libraries, thus the data must be loaded from a fixed location.
I propose to read the file from the same directory where the library is located (so the user can copy the library to custom location where her data sits).
We can also customize the data location through the environment variables, but that requires restarting Uppaal.

1. libtable reads table.csv with a number of rows and columns separated by comma and implements the following functions:

int read_int(int row, int column);
double read_double(int row, int column);

2. libdictionary reads dictionary.csv with at least two columns and implements a lookup based on the first column based on key value and returns the value from specified column on the same row:

int lookup_int_for_int(int key, int column);
int lookup_int_for_double(double key, int column);
double lookup_double_for_int(int key, int column);
double lookup_double_for_double(double key, int column);

3. libtrajectory reads trajectory.csv with similar structure as dictionary, except the first (key) column values are monotonically increasing and the key and trajectory values linearly interpolated:

double lookup(double key, int column);

The "-O csv" outputs plots in CSV format with GNU Plot scripts so that the plots similar to ones in a GUI can be rendered externally, also the CSV files can be read in other tools.
The issue is that the "-O csv" option has no effect on the Pr[] query output.

The "-O csv" should produce CSV files with plot script also for Pr[] queries

Describe the bug
On Linux, if UPPAAL is installed in a path that includes spaces, it gives OS errors for the GUI and file not found errors for verifyta/server.

To Reproduce
Install UPPAAL on a path similar to:

/home/user01/My Dir With Spaces/uppaal
open the GUI or execute verifyta / server directly

Expected behavior
It should just work

Desktop (please complete the following information):

• OS: Linux
• Version: 4.1.24 (also doesnt work on 4.0.13 but gives different errors)

Additional context
Example errors:

./server: line 10: /home/user01/My: No such file or directory
It just cuts off at the dir with spaces, so I am guessing the path string is not formatted correctly for Linux? I.e. not escaping spaces properly.

Is your feature request related to a problem? Please describe.
currently it is not possible to zoom-in into plots and inspect the small data, especially when it is dwarfed by a magnitude larger signals.

Describe the solution you'd like
The plot should offer some way to magnify the trajectories and shift to different portions of the plot.

Additional context
Uppaal also implements value filtering which hides small or fast changes in the signal.
So in cases with lots of data, the zoom-in/out should be adaptive and perhaps request the engine for additional information.