Hello Jiri and Peter

The last week has been spent on looking into several different topics, in order to get a clear idea of what we want to pursue as our semester project this semester. In particular we have looked at the following topics:

1. Code Generation -- Going from Petri nets to code
2. Code Verification -- Going from code to Petri nets
3. Two player timed workflow games
4. Overapproximation by constraint solving using SMT techniques
5. Precompiled successor generation -- Verifying specific property of a Petri net by compiling a custom model checker that verifies only that the property holds on the given net

We have come to the conclusion that we do not want to pursue the topic of _overapproximation_ (4) any further, and unfortunately, we have not yet had the chance to look too deeply at _Precompiled successor generation_ (5). _Code generation_ (1) is also an area in which we wish to conduct a bit more research before taking a decision

As it stands here is what we find interesting to do within each topic (should we pick it as our semester project). We've written a short summary of our research below.

---

## 1. Code Verification

The goal of this preliminary research was to determine if it is possible to answer some questions about some source code, by first faithfully converting the program to a Petri-Net, and then verifying the property on the net, instead of the code.

There exists some tools that use Promela to do this:
* JavaPathFinder & Brandera translates Java source code into Promela language which is the input language of SPIN
* Feaver produces Promela from C programs
* VeriSoft

In this regard, I present 2 papers talking about this.

### Transforming sources to petri nets: a way to analyze execution of parallel programs

[Transforming sources to petri nets: a way to analyze execution of parallel programs](https://dl.acm.org/doi/10.5555/1416222.1416240)

Questions one could ask about a program can usually be divided into different perspectives. One such question could, e.g., be if the program terminates. In this case, then the control-flow perspective would be apt. From this, we could imagine, that we could choose one perspective at a time to answer a specific question. In this way, the combinatorial explosion is mitigated. Some more examples of perspectives could be:
* Control-Flow Graph (program’s structure)
* System calls Sequences,
* Synchronization Mechanisms,
* Array bounds,
* User-defined invariants, and
* I/O behaviors

### Construction of Petri net based models for C programs

[Construction of Petri net based models for C programs](https://cse.iitkgp.ac.in/~chitta/pubs/rep/thesisKulwant.pdf)

Compilers are unfortunately often difficult to work with because of the optimizations they promise. The compilers should verify that the optimized program is behaviourally equivalent to the original, which is difficult. Apparently Petri-Net are very good for this purpose.

Instead of using Petri-Nets, the author uses a formalism called _PRES+_, which stands for Petri net based Representation of Embedded Systems. It's an extension to Petri-Nets, which allow for input-places, output-places, variables, expressional assignments, and guards.

The workflow presented in the paper:

Limitations:
* Only integer variables and arrays must be used.
* Every `scanf()` and `printf()` call must read and write exactly one integer variable respectively and there must not be any other function calls.
* The program must contain exactly one function i.e. `main()` with `void` as its return type.
* The program must not contain any `goto` statements (although the intermediate cfg may contain such statements).

### Conclusion

As far as I could tell, there does not exist anything that can translate source-code to normal Petri-Nets with Inhibitor arcs without large limitations (e.g. perspectives). Even though there seems exist some work in the area, this seems to be a good niché to work on.

As a long term vision, it would be pretty cool to have an option in TAPAAL under the import menu, where the user could import Java-code (or some other source code). Being able to verify certain properties of "real" programs using TAPAAL would also be pretty cool

Challenges:
* Recursion: How to handle the "call-stack" in a acceptable way.
* Strings: How to represent things of variable length and domain. Maybe Colored PNs would work great here?

---

## 2. Two player timed workflow games

We made an (we hope) exhaustive literature search for workflow games for any number of players and we didn't find anything concrete. The only vaguely related thing we found, was a paper using colored Petri nets to assign roles to actors, in order to model the situation where there's only certain kinds of people that are able to execute certain kinds of actions in a workflow. Other than that we were not able to find anything that dealt with the notion of players on the level of Petri nets. We searched for the literature in the following places:

* Applications and Theory of Petri Nets and concurrency year 2007-2020
* Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data year 2015-2020
* dblp and Google scholar, where we searched for
* Workflow games
* MAS Petri nets
* Petri agent
* Petri workflow agent
* Workflow agent
* Petri workflow net agent
* Wil van der aalst
* Wil van der Aalst's homepage

The initial idea we have for this project is to first take the notion of players and apply it to workflow nets. The workflow nets we reference here is the ones defined in van der Aalst's classic paper: [The application of Petri nets to workflow management](https://www.worldscientific.com/doi/abs/10.1142/S0218126698000043). After that we can take two routes. Either we first implement the newly defined theory into TAPAAL and then add more constructs into the theory (time guards, age invariants, and so on) until we have all the theoretical constructs that TAPAAL offers. After that we implement the extra constructs into TAPAAL.
Or we add the extra constructs in the theory first and then implement the everything into TAPAAL.
Ofcourse, the order depends entirely on a multitude of factors (how is workflow TAPAAL engine constructed, how long does it take to get theory into place, etc.), however this is just an initial view of the project.

---

## 3. Code Generation

We wanted to find out if it is feasible to automatically generate code from a Petri net. The generated code could either be inferred from the behaviour of the model, and thus be generated as unit tests, or it could just be generated directly into source code. As mentioned above, this area is one where we want to research a little bit more before taking a decision on it. Some examples of papers in this area could be:
* [Towards Automatic Code-generation from Process-partitioned Coloured Petri Nets](https://cs.au.dk/fileadmin/site_files/cs/research_areas/centers_and_projects/cpn/paper03.pdf), where they compile CPN down to Erlang.
* [A Tool for Automated Test Code Generation from High-Level Petri Nets](https://link.springer.com/chapter/10.1007%2F978-3-642-21834-7_17)

---

## Conclusion
As you can probably tell, we are a bit inconclusive about what we want to work on for this semester project, however we expect to narrow the list of topics down to at least two topics before our meeting.
On the meeting on wednesday we will tell you the updated list of topics and then we will start a dialog on which topic to choose, which will result in a decision from us.
We are very excited to see you on wednesday.

Kind regards
sv904e20