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.).

Filter by
Sorted by
Tagged with
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 ...
Lqs66's user avatar
  • 11
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 ...
MicroEnder's user avatar
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 ...
lynn's user avatar
  • 1
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 ...
imranalialvi's user avatar
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, ...
Steve Linton's user avatar
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 ...
Nitish Yadav's user avatar
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 ...
Renaud Pacalet's user avatar
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 ...
Aqs Khan's user avatar
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 ...
Lucent's user avatar
  • 33
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 ...
Scarlett's user avatar
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
Yasmine's user avatar
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 ...
giudaballerino's user avatar
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 (...
Renaud Pacalet's user avatar
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....
Jaime Cuartas's user avatar
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 ...
eric's user avatar
  • 11
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(...
Robb1's user avatar
  • 4,597
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 ...
giudaballerino's user avatar
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 ...
eric's user avatar
  • 11
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 ...
Nuhil Mehdy's user avatar
  • 2,424
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 ...
Mickaël's user avatar
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....
mkaltw's user avatar
  • 3
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 ...
Josi's user avatar
  • 5
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 ...
Josi's user avatar
  • 5
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 ...
Arooj Nawaz's user avatar
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....
Satarupa's user avatar
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....
waqas's user avatar
  • 1
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 (...
b_doma's user avatar
  • 1
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 ...
Huddlespith's user avatar
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. ...
Zordan's user avatar
  • 45
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?
MrDank's user avatar
  • 2,030
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 ...
Markovchain's user avatar
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 ...
Qhz's user avatar
  • 1
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 ...
Michael Eder's user avatar
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.
OmG's user avatar
  • 18.4k
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: ...
OmG's user avatar
  • 18.4k
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 ...
Liam's user avatar
  • 21
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) { ...
user2083098's user avatar
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 ...
Alexander's user avatar
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 ...
Heinrich Ody's user avatar
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 ...
user993257's user avatar
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 ...
Michael Eder's user avatar
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 ...
user993257's user avatar
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 (...
user993257's user avatar
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 ...
med talel's user avatar
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 ...
J. Loe's user avatar
  • 201
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 ...
Robert Ruska's user avatar
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/...
Michael Eder's user avatar
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; ...
Michael Eder's user avatar
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 ...
Muhammad Abdul Basit's user avatar
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 ...
Mathay Kahraman's user avatar