Skip to content

Commit

Permalink
minimal ci
Browse files Browse the repository at this point in the history
  • Loading branch information
thorstink committed Nov 18, 2023
1 parent 0362619 commit d36331b
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 30 deletions.
18 changes: 6 additions & 12 deletions .github/workflows/config.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,30 +7,24 @@ jobs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v1

- name: apt dependencies
run: |
sudo apt update
sudo apt install -y ninja-build
- name: "build project"
run: |
git submodule update --init --recursive
mkdir build
cd build
bash -c 'cmake -GNinja -DCMAKE_BUILD_TYPE=Release -DBUILD_EXAMPLES=ON ..'
ninja
bash -c 'cmake -DCMAKE_BUILD_TYPE=Release -DBUILD_EXAMPLES=ON ..'
make
- name: "tests with ASAN"
run: |
cd build
bash -c 'cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON -DASAN_BUILD=ON -DTSAN_BUILD=OFF ..'
ninja
bash -c 'cmake -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON -DASAN_BUILD=ON -DTSAN_BUILD=OFF ..'
make
ctest -VV
- name: "tests with TSAN"
run: |
cd build
bash -c 'cmake -GNinja -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON -DASAN_BUILD=OFF -DTSAN_BUILD=ON ..'
ninja
bash -c 'cmake -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON -DASAN_BUILD=OFF -DTSAN_BUILD=ON ..'
make
ctest -VV
33 changes: 17 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,25 +26,28 @@ This Petri net can be described using Symmetri:

```cpp
using namespace symmetri;
Net net = {{"foo", {{"B", "C"}, {"Z", "B"}}},
{"bar", {{"Z"}, {"B", "C"}}}};
Marking initial = {{"Z", Color::Success}};
Net net = {{"foo",
{{{"B", Color::Success}, {"C", Color::Success}},
{{"Z", Color::Success}, {"B", Color::Success}}}},
{"bar",
{{{"Z", Color::Success}},
{{"B", Color::Success}, {"C", Color::Success}}}}};
Marking initial = {{"Z", Color::Success}};
Marking goal = {};
auto pool = std::make_shared<TaskSystem>(4);
PetriNet app(net,"test_net_without_end", pool, initial, goal);
auto task_system = std::make_shared<TaskSystem>(4);
PetriNet app(net, "test_net_without_end", pool, initial, goal);
app.registerCallback("foo", &foo);
app.registerCallback("bar", &bar);

auto result = fire(app); // run until done.
auto log = getLog(app);
auto result = fire(app); // run until done.
auto log = getLog(app); // get the event log
```
- `net` is a multiset description of a Petri net
- `store` is a lookup table that links the *symbolic* transitions to actual functions
- `priority` can be used if some transitions are more equal than others ([Wiki on prioritized Petri nets](https://en.wikipedia.org/wiki/Prioritised_Petri_net))
- `m0` is the initial token distribution (also known as _initial marking_)
- `pool` is a simple task based threadpool
- `app` is all the ingredients put together - creating something that can be executed! it outputs a result (`res`) and a log (`eventlog`)
- `initial` is the initial token distribution (also known as _initial marking_)
- `goal` is the goal marking, the net terminates if this is reached
- `task_system` is a simple SPMC-queue based based threadpool
- `&foo` and `&bar` are user-supplied *Callbacks*
- `app` is all the ingredients put together - creating something that can be *fired*! it outputs a result (`res`) and at all times an event log can be queried
## Build
Expand All @@ -64,9 +67,7 @@ make && make test
## Run examples

```bash
# assumed you build the examples
# finishes with a deadlock
./build/examples/hello_world/symmetri_hello_world nets/passive_n1.pnml nets/T50startP0.pnml
# assumes you build the examples
# finishes by reaching the final marking (e.g. completed). Use keyboard to interact pause/resume/cancel/print log
./build/examples/flight/symmetri_flight nets/PT1.pnml nets/PT2.pnml nets/PT3.pnml
```
Expand Down
21 changes: 21 additions & 0 deletions docs/symmetri_lib.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,24 @@ make test
```

## Architecture

Symmetri was built with the the idea to serve as an abstraction at the *behavioral* level. Petri nets encode execution protocols that are built from smaller building blocks. The smaller building blocks could be Petri nets or some other piece of executable (*fireable*) code, shaped in the form of *callbacks*. In theory the smallest transitions could be simple functions such as "pop data from queue" or something of similar complexity. In practice we envision more elaborated transitions such as *take photo* for example. The main motivators for this self-imposed distinction is twofold.

Firstly, there is a performance penalty on wrapping everything in transition-blocks. The penalty is partly that the execution of the transition-bound callback is dispatched to a threadpool (adding latency), also in order for a transition to be fired, it needs to be checked to see if it is fireable. Checking whether a transition is enabled is not expensive, but it can easily overshadow the payload if that is very small (e.g. a small function).

The second reason for placing the transition at the behavorial level is to mitigate the scalability issues that are inherent to Petri nets. Petri nets offer many formal analysis techniques. but Petri nets with infinite loops, or simply a lot of places and tokens have a huge if not infinitely large reachability graph. This renders the formal analysis unfeasible. By keeping the Petri nets small and bounded it stays feasible to give some insight on their workings.

### The Symmetri eventloop

WIP
### Callback execution

WIP
### Determining the active transitions

WIP

<div>
![](img/architecture_light.svg)
<center><br />This dataflow layout of the Petri net library.</center>
</div>
4 changes: 2 additions & 2 deletions docs/symmetri_nets.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@ Because callbacks can have variable durations before they generate a result and
Not having to define every possible sequence can be a work-saver, however, it can be interesting to retrospectively inspect the actual executed transition sequence. For this Symmetri creates an event log. Symmetri’s event log definition is inspired by the [definition used in Process mining](https://en.wikipedia.org/wiki/Process_mining#:~:text=Input%20for%20process%20mining%20is,and%20(3)%20a%20timestamp.);

Each event in the log should contain:
- a unique identifier for a particular process instance (called case id),
- an activity (description of the event that is occurring), and
- a unique identifier for a particular process instance (called case id)
- an activity (description of the event that is occurring)
- a timestamp

In Symmetri the unique identifier consists out of an identifier for the transition and an identifier for the parent Petri net the transition is a part of. This combination guarantees that we have an unique identifier also in nested Petri nets. The activity in Symmetri is considered more as the state changes during the firing “lifecycle”. This means the event log is populated mostly with scheduled, started, completed. The timestamp is based on a monotonic system clock.
Expand Down

0 comments on commit d36331b

Please sign in to comment.