Questions tagged [uppaal]
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
82
questions
0
votes
0
answers
7
views
Can UPPAAL get all the counterexamples?
When I enter A[] not Automata.locationA in the validation screen for reachability analysis, I can get a symbolic trace (counterexample) when the model doesn't satisfy the property, sometimes there is ...
0
votes
0
answers
24
views
How to make UPPAAL use the strategy I wrote when doing verification?
I'm a student now using UPPAAL for academic research.For some reasons, I want to write some strategies to optimize the process when UPPAAL verification.
I mean, if I have a search strategy specific to ...
0
votes
0
answers
117
views
How to implement UPPAAL external function files in calls to python scripts
How to implement UPPAAL external function files in calls to python scripts. Functions that use python scripts in dynamically linked cpp files, such as Py_Initialize(), will report an error.
Syntax ...
0
votes
0
answers
66
views
UPPAAL: Conversion of C/C++ code into model
can we convert C/C++ code into models (FSM etc) so that afterwards UPPAAL can be used for verification? Does UPPAAL or any other tool offer this feature?
Thanks
I tried online forums and google but ...
0
votes
0
answers
89
views
Is threre a version of uppaal for Apple Silicon
When I download the mac version of uppaal The jar file runs but produces an immediate index out of bounds exception. The most obvious reason for the problem is that my mac is apple silicon, not intel, ...
0
votes
1
answer
44
views
Converting double to integer using fint() is not working. Is there any alternative for this?
I want to convert 1.8 to 2.0 and then change the type of the result to an integer value i.e., 2. To do this, I execute the following function for the shown template.
int xx;
double dx=round(1.8);
void ...
0
votes
0
answers
37
views
How to refer to the current location of a process in the guards of another process
I am currently modelling a system with several processes using UPPAAL Stratego. In some of these processes I'd like to guard edges with the current location of other processes, e.g., main.running and ...
0
votes
0
answers
67
views
XML used in Uppaal Expert
I need guidance how can i represent edges ,nodes ,labels ,assignments ,conditions in organized way On Uppaal while uploading a XML file . My project is basically conversion of C to XML(xml that ...
0
votes
1
answer
184
views
A simple UPPAAL model but can't get result due to the range of an integer variable
This uppaal model showing in the image is part of a top system.
It's used to check the condition var==1 hold for at least 10 time units. The range of the integer variable var is [0, 20000].
I use ...
0
votes
1
answer
145
views
Clock guards and deadlocks
I'm using UPPAAL for an academic project and I have some questions. I have to design a timed automata so my model has invariants on locations and clock guards on the edges. The problem is I must also ...
0
votes
1
answer
69
views
Uppaal : Is there a way to know the size of the state space?
In Uppaal, is there a way to know how many states exists as the combination of locations and variables
1
vote
1
answer
162
views
What is the difference between Symbolic and Concrete model checking when the search is bounded in time?
Could someone please spend a few words to explain to someone who does not come from a formal methods background what is the difference between verifying a specification using Symbolic Model Checking ...
0
votes
1
answer
117
views
Trace format from verifyta not compatible with tracer utility of libutap library
I am currently trying to automate model checking experiments with UPPAAL. As I plan to run thousands of tests the GUI is not an option. So I tried to use verifyta (version (Academic) UPPAAL 4.1.25-5 (...
0
votes
1
answer
219
views
Is there any way to know if an uppaal model recognizes a trace?
I am trying to check if an uppaal model recognizes a trace.
I have to generate random traces and check if another similar model can do the same trace. I can do the random generation by using verifyta....
1
vote
1
answer
128
views
deadlock caused by two urgent locations
a small exampleDuring the simulation, I find that if one state is in urgent location, the other state is about to reach urgent location, and it will deadlock. And I want to verify the upper and lower ...
0
votes
1
answer
430
views
Declaration of multiple processes from the same Template in Uppaal
Is there a way to instantiate multiple processes obtained from the same Template in Uppaal?
For example currently I write (in the System declarations file):
// Template instantiations
P1 = Template(...
0
votes
0
answers
177
views
Counterxample enumeration on UPPAAL
Good afternoon, I am doing some experiments with UPPAAL model checker and my understanding is that, when a property is not verified, the verification engine (verifyta) only enables to find one among ...
0
votes
1
answer
46
views
The supper cannot be verified
Why does this happen when I verify. When I verify the sup of test1.P3 and test.P6, I get gtr < inf. What does this mean and how can I solve it? My model is as follows:
enter image description here
...
0
votes
0
answers
190
views
UPPAAL is not showing trace if the property is not satisfied
I am using UPPAAL 4.1.24 for modeling a simple system composed of 1 main process and 3 observer processes. The main process uses a broadcast channel which is listened to by the observer processes. I ...
1
vote
2
answers
454
views
Uppaal - How to force a transition when a condition becomes true?
I would like to be able to force a transition as soon as a condition becomes true.
For example in this Example, I would like to force the transition from the system next from the state S0 to S1 as ...
0
votes
2
answers
217
views
UPPAAL: ModelDemo for Java API (Error while getting memory info: 34, javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3])
I am trying to get get the ModelDemo.java to work because I would like to work with the Java API. Unfortunately, I am running into errors...
I am using Eclipse IDE Version 2020-06 (4.16.0), openjdk 11....
0
votes
1
answer
183
views
how to convert double values to integer with int fint (double) without getting 'Server connection lost' in Uppaal
I want to convert double values to integer to use them in the guards of the model.For this I found the int fint (double) function at https://www.it.uu.se/research/group/darts/uppaal/download.shtml and ...
0
votes
1
answer
193
views
How to save variables from Uppaal created during the modeling process
I've created a model with Uppaal in which several integer variables change over the course of time. Now I would like to save the values of the variables during the modelling process somewhere (best in ...
0
votes
1
answer
180
views
UPPAAL - Query Regarding Channel Related Property
I am trying to make properties in which channels are used for example if X Channel signal is transmitted then this implies that Y Channel should send signal in response but I am facing an issue while ...
0
votes
1
answer
166
views
UPPAAL- Generate some strategy
I have been using Uppaal Stratego for some time now. I have generate strategies using verifyta cli and used command like --print-strategies pathtoShowStrategy file.
Now my strategy produced is of 416....
0
votes
0
answers
60
views
Unable to verifiy TCTL properties?
i built this template in UPPAAL 4.1 version. We can see in fig1, there exist a single path where agent can perform ReflexProcessing, but when i write given property
E<> not (MonitorAgent....
0
votes
1
answer
202
views
UPPAAL Verifier
I have a model in the UPPAAL software, and try to verify whether items[2] == 3 in every case. I've tried with that:
A<>(items[0] == 0 and items1 == 0 and items[2] == 3)
I made a "closing" state (...
1
vote
3
answers
715
views
Installing Uppaal on Mac OS
I'm trying to install Uppaal on my Mac. I have Catalina installed and I am aware of the workaround posted on here to do with authorisation and have done this.
But when I run the Uppaal script I get ...
0
votes
1
answer
146
views
Can't find what could cause the "caused by an out-of-range assignment or out-of-range array lookup." error
I get this error when I try to check my system for deadlocks:
The verification was aborted due to an error. Most likely, this is
caused by an out-of-range assignment or out-of-range array lookup.
...
3
votes
3
answers
2k
views
Check whether OS is supported error in Uppaal 4.1.23 on Mac OS Catalina 10.15
I installed Uppaal 4.1.23 on Mac OS 10.15 but I get an error. What do I do?
1
vote
1
answer
2k
views
Multiple Synchronizations in UPPAAL
how can I model multiple synchronizations in UPPAAL? For example: The state change triggers two other state changes at the same time in different templates. In the synchronization field, I can only ...
0
votes
0
answers
308
views
Problem with running Uppaal 4.1.22 in Mac OS
I downloaded and installed uppaal 4.1.22 on Mac OS 10.14. I have Java 8 installed.
When opened the uppaal.jar, a window pops out saying “server exited with error 126. Check OS.” After I close the ...
1
vote
1
answer
341
views
UPPAAL SMC motivating example
I want to understand the UPPAAL SMC example discussed in [1].
Here is the UPPAAL-SMC example:
The three timed automata should visualize the probability distribution in UPPAAL SMC. In the paper it ...
0
votes
1
answer
152
views
Read/Write Data from/to File in Uppaal (For Data Log)
How to write some data into a file as a log or some statistics in Uppaal?
Is there any fprintf function or some FILE* such as we have in C or not? The same question for reading from the file too.
0
votes
1
answer
730
views
Array Initialization In Uppaal
I have the following struct:
const int MAX = 6;
typedef struct {
int num1;
int arr1[MAX];
int arr2[MAX];
int num2;
} MyStruct;
And I initialize this array likes the following:
...
0
votes
1
answer
367
views
Value passing through channels
According to
http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf
There is no value passing through the channels but this is easily encoded by shared variable: define globally a ...
0
votes
1
answer
130
views
CSP-like synchronizations
I'm trying to use CSP-like synchronization mechanism and I don't understand why the initial state of the following model is a deadlock:
const int N = 2;
chan a;
process Processes(int [1,N] pid) {
...
0
votes
1
answer
52
views
What if Uppaal removes relative time?
I hope someone here can give me your advice or knowledge.
I have already read about train-gate example in Uppaal and in Spin. I also tried to use Uppaal for verifying my plans, and the results were ...
1
vote
2
answers
767
views
Understanding Urgent Channels in Uppaal
I have three automata (see below), the single global declaration urgent chan u; and the system declaration system UrgentChannel, P1, P2;. My understanding is that by making u an urgent channel, the ...
0
votes
1
answer
2k
views
How does Uppaal clock evolve? I have two locations 1 and 2 without invariant. What is clock value?
How does Uppaal clock evolve? I have two locations 1 and 2 without invariant, a clock reset to zero (0) on the transition into location 1. On the edge between location 1 and 2, how do I know the value ...
0
votes
1
answer
288
views
UPPAAL SMC avoid State Space Explosion
I am trying to query a larger system with UPPAAL SMC and it ends up with a "memory exhausted" error message. By nature, UPPAAL SMC should not result in a state space explosion that's why I am asking ...
0
votes
1
answer
177
views
How to make all the receiving! edge in Uppaal receive the channel? at once
I have a system with 5 processes. One of the processes sends signal1! to 3 processes(That is the 3processes receive signal1?). But when I simulate only one of the 3 receiving processes received ...
0
votes
0
answers
419
views
Uppaal simulation Error : state not well define
I am new to uppaal. I have a system consisting of different models. I also have a clock and a double variable declared.
For my invariants and guards, there is a need for me to check these two values (...
0
votes
1
answer
57
views
can you decalare a json array in uppaal?
I am trying to model an ATM system in uppaal and I want to use a json array like a database for card_IDs and pin numbers like this :
[ {
id : 12548,
pin: 1244
}]
is this possible or ...
0
votes
1
answer
711
views
Uppaal Verification not working as intended
So I'm trying to run a very simple verification on my model, however I get a message saying the property is not satisfied.
I'm trying to verify that in my model if ever Person(0) goes In eventually ...
0
votes
1
answer
215
views
Simple basic verification problem in uppal
I'm struggling with some simple verification. I have automata and value x like this:
automata2
When x at the start is different from 0 then E<> x !=0 is satisfied, but when x = 0, then its not ...
1
vote
1
answer
747
views
How to cast a double value to a integer value in UPPAAL?
How it is possible to cast a double value to a integer value in uppaal?
double rand;
rand = random(2);
int i;
i = (int) rand;
According to the API documentation (http://www.it.uu.se/research/group/...
1
vote
1
answer
979
views
How to return an array in UPPAAL?
I am trying to return an integer array in an UPPAAL function.
What is the correct syntax for that?
This code snippet doesn't work:
int[] randomTest(int N)
{
int test[2];
test[0] = 0;
...
0
votes
1
answer
655
views
Unable to verify UPPAAL properties
I am verifying a very small model. But I receive the memory exhaust message. I changed the model several times but having same problem.
I thought that problem would be due to using a user defined ...
1
vote
1
answer
491
views
Unbounded delay but no positive rate
I have created this UPPAAL specification: https://pastebin.com/v4AkYUuy
But when running the query:
simulate 100 [<=500] { time }
I get the error:
Location Person.Rijssen has unbounded delay ...