search

koluacik / uppaal-py

UPPAAL wrapper for Python
MIT License
5 stars 0 forks source link

Any ideas about how to add new feature 'product of two or more TA' ? #1

Open ziji-wu opened 2 years ago

ziji-wu commented 2 years ago

README told that the feature of 'product of two or more TA' is not supported now. However, that is a vital feature I need in my project, so how can I add this new feature if I want? Is it hard?

Unfortunately, I have no idea how to realize it, could some one helps? Thanks a lot.

koluacik commented 2 years ago

Hello @ziji-wu, I believe analysis on network of timed automata is doable. First let me provide some context:

The library provides an algorithm for checking path realizability for a given timed automaton. A linear programming problem is constructed to determine the amount of time spent on each "location" subject to location invariant and transition guard constraints if such solution exists. I assumed that there exists only one TA in the system for simplicity while working on the project.

In theory, constructing a timed automaton (TA_1 x TA_2) from a system of timed automata with TA_1 and TA_2 is quite simple. You can find examples of such constructions in the literature. Doing so in UPPAAL might be daunting for any nontrivial system, so maybe you can do that programmatically.

ziji-wu commented 2 years ago

Hi @koluacik, thank you very much.

Besides, from the Definition 3 (Semantics of a network of Timed Automata) of the UPPAAL Tutorial, I noticed that semantics between (TA_1 x TA_2) and NTA with two Templates TA_1 & TA_2 seems to be the same, is that right?

If that is True, that means one can realize the future of 'product of two or more TA' simply by adding function 'add_template()' to 'NTA' object and expand the system declaration and queries at the same time, and others can be done by UPPAAL.

Thanks a lot again!

koluacik commented 2 years ago

Yes, the definition you linked is the one I was talking about. The semantics of the "system" should be preserved by constructing a single "template". You still need to pay attention to synchronous and asynchronous channels and shared variables etc.

If that is True, that means one can realize the future of 'product of two or more TA' simply by adding function 'add_template()' to 'NTA' object and expand the system declaration and queries at the same time, and others can be done by UPPAAL.

Thinking about it, it should be possible to construct a product of TA instantiated from the templates inside the NTA object. Then you would end up with the semantic equivalent of a network of TA. That being said doing so might require almost complete rewrite of the library.

I initially implemented the library to work on a heuristic solution for TA relaxation for reachability problem. My main focus was singular TA with basic clock expressions so I did not focus on a robust implementation that supports the full range of UPPAAL specifics. At the very least, actual template instantiations should be read from the system declaration and shared and private clocks and variables should be differentiated. Getting individual TA templates from the internal representation of the system of TA in the NTA object to write back the modified system to xml is a whole another story.

You can fork this project to implement the TA product construction. Feel free to reach out if you need anything else.