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.).
77
questions
0
votes
0
answers
14
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 ...
-1
votes
0
answers
27
views
Query in UPPAAL for max and min time
I have a UPPAAL model with 2 clocks: t and totalTime. "t" is a variable I use for guards and invariant on locations. "totalTime" is a clock I don't update among the flow and its ...
0
votes
1
answer
22
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
42
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
0
answers
28
views
Semantics of Timed Games and Channel Synchronisation in UPPAAL
I'm struggling to understand how timed games work together with (broadcast) synchronization in UPPAAL (TiGa / Stratego). Imagine the following example:
Forcing the environment
Here, the edge ...
0
votes
1
answer
32
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
0
answers
61
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
53
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
150
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....
0
votes
1
answer
62
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
178
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
88
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
37
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
98
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
202
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
161
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
123
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
138
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
86
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
116
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
48
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
122
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
435
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
110
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
2
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
1k
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
202
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
250
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
111
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
530
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
176
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
74
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
41
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
486
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
246
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
98
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
330
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
53
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
438
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
126
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
568
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
748
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
486
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
388
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 ...
1
vote
1
answer
417
views
Uppaal: Probability estimation in train gate example
I am running Train Gate example, and I want to run a verification property
Pr[<=100] (<> Train(0).Cross)
Saying what is the probability of Crossing of Train(0) in 100-time units.
I have added ...
0
votes
1
answer
462
views
UPPAAL Verification Error- Index value is out of range
I am using Uppaal for system verification. The simulation is running perfectly fine but when I verify by using this property A[] not deadlock it is giving me the following error:
_The successors of ...
0
votes
1
answer
736
views
Uppaal template parameters
I am using UPPAAL 4.1.19 and I am following the train tutorial, given in this. In Train template, I put the parameters int[0,N] e, const int id and in the system declaration I declare Train1=Train(el, ...
1
vote
0
answers
35
views
Relationship between explored states and utilized memory in model-checking
What is possible relationship between states and utilized memory in model-checking. Can we estimate total memory that can possibly be utilized by our model (state space) before actually implementing ...
0
votes
1
answer
57
views
how can i reset my automaton in the UPPAAL
i created some automaton in the UPPAAL model checking tool, and there is a dialog between them. when an error occurs in one of them,other must be reset.
i can't put return edge for all the nodes to go ...