Support for weights on all arcs

[Mathias Grund Sørensen]

For full compatibility with TAPAAL, VerifyPN should support weight on all arcs. Currently, weights/inscriptions on the following arcs are not supported:

Transport Arcs:
Weights on transport arcs are currently disregarded when decomposing into in- and outgoing arcs in the model parser and the weight is fixed to 1. The weight of the transport arc should be propagated to both replacing arcs.

Inhibitor Arcs:
TAPAAL supports weighted inhibitor arcs as well. Is it possible to add this support to VerifyPN?

[Jonas Finnemann Jensen (jopsen)]

Okay, so please provide two minimum examples... With associated queries that are not answered correctly.
This thing is definitely something we can add to the current test suite.

Weighted Transport Arcs
====================
Also please document how weight are written on transport arcs, as well as their untimed semantics. Just to be clear, from looking at the code, it looks like a transport arc goes into a transition and out of the transition. Where as a normal arc is either a in-arc or a out-arc. Is it correct that a transport arc is both.
And is it possible to have both transport arc and normal arcs between the same transition and place, in both the output and input case?

As Mathias says, this looks like an easy hack, just adding the part from `parseArc` that handles inscription to `parseTransportArc`.
Assuming the semantics are correct. Ie. transport arc from p1 to t1 to p2 with weight k, is equivalent to in-arc from p1 to t1 and out-arc from t1 to p2, where both in- and out-arcs have weight 2.

Weighted Inhibitor Arcs
===================
Again, I need semantics refreshed :)
So is it correct that an inhibitor arc with weight k from p1 to t1, inhibits the firing of t1, if p1 has k or more tokens?
Thus, unweighted inhibitor arcs have weight 1 and requires that the place has zero tokens before the transition can fire.
And a k-weighted inhibitor arc requires that the place has strictly less than k tokens before the transition can fire.

I think this is easily implemented too... By extending the `InhibitorArc` structure with a weight field and using this for construction of the transition pre-condition in `PNMLParser::parse`.

Anyways, if you can write some examples that will make it easy for me to verify that it works, I might be able to get this done before I relocate on Tuesday, otherwise it might take another week or so...

[Mathias Grund Sørensen (mathias.grund)]

Hi.

I have provided a minimum example for each case.

> Weighted Transport Arcs
> ====================
> Also please document how weight are written on transport arcs, as well as their untimed semantics. Just to be clear, from looking > at the code, it looks like a transport arc goes into a transition and out of the transition. Where as a normal arc is either a in-arc or > a out-arc. Is it correct that a transport arc is both.

Yes, that is correct. The timed semantics are that the tokens (i.e. their age) are transferred from one place to the other when the transition fires (guards/weights on transport arcs as well as all other ingoing arcs must be satisfied to fire). So in untimed semantics, this is equivalent to just having the in and out arc separately. Weights indicate how many tokens are moved.

> And is it possible to have both transport arc and normal arcs between the same transition and place, in both the output and input > case?

No, you can not have a transport arc P1 --> t --> P2 and also a normal arc P1 --> t or t --> P2.

> Weighted Inhibitor Arcs
> ===================
> Again, I need semantics refreshed :)
> So is it correct that an inhibitor arc with weight k from p1 to t1, inhibits the firing of t1, if p1 has k or more tokens?
> Thus, unweighted inhibitor arcs have weight 1 and requires that the place has zero tokens before the transition can fire.
> And a k-weighted inhibitor arc requires that the place has strictly less than k tokens before the transition can fire.

Yes, all three correct.

The attached models are generated so that they represent weight as inscriptions in the same way as it is done with in/out arcs, so the same parsing logic should be applicable.

Let me know if you want some more models for testing.

[Jonas Finnemann Jensen (jopsen)]

Wow, that was quick feedback... Thanks!

I'll try to take a quick look at it tomorrow...

Also, if you'd like a commandline flag for disabling over-approximation, just file a bug, this would be trivial to add...

[Jiri Srba (srba)]

Yes, the answers are 100% correct. Thanks Mathias.

For untimed semantics there is no difference between normal and transport arcs and it is impossible to have both
at the same time from a given place to a given transition.

The semantics of inhibitor arcs is also correct and it is impossible to have between a given place and transition
both inhibitor and other type of arcs.

I asked for the flag, it will be useful for testing the engine.

One last question, does the current parser support PNML input syntax of nets?

[Jonas Finnemann Jensen (jopsen)]

@Jiri,
What is "PNML input syntax of nets".
Note: At some point you should consider documenting the TAPAAL-specific PNML format, it is non-trivial to
see that inscriptions are weights .

> For untimed semantics there is no difference between normal and transport arcs...
Sure there is, a normal arc is either an in-arc or an out-arc, a transport arc encodes both an in-arc and an out-arc, right?
(But yes, semantically a transport arc can be replaced by an in-arc and an out-arc).

[Jiri Srba (srba)]

Yes, we should document the TAPAAL xml syntax (on todo list). I was asking whether verifypn can read the PNML standard
syntax for untimed nets (like the ones that were distributed for the competition). This would make it easier
to communicate with other tools for untimed nets. If this is the case, I would suggest that we export the nets
from TAPAAL in this syntax directly.

Yes, transport arcs are meant as a pair of two arcs tight together. Indeed, in the untimed syntax they are the
same as an input arc and output arc.

[Jonas Finnemann Jensen (jopsen)]

> the PNML standard syntax for untimed nets
Maybe, I think the PNML standard syntax for untimed nets is pretty vague on how weights should be specified.

If think that standard PNML is a strict subset of TAPAAL-PNML... I can't access PNML specification, but from the examples
I would think that we do parse standard untimed PNML correctly.
But I wouldn't recommend submission to contests without testing this... If you do so, feel free to add such standard PNML syntax tests to the Test/ folder, see README.mkd for instructions on how to name them correctly.

[Jiri Srba (srba)]

Thanks, I think we will have a look at the PNML format soon. Some users requested export to this format for the use
with other tools.

Btw. does verifypn support or could support deadlock proposition (valid if no transition is enabled at all)?

[Jiri Srba (srba)]

Sorry, it does support deadlocks (but not in the overapproximation). I got confused.

[Jonas Finnemann Jensen (jopsen)]

Hmm... Maybe it's just me getting old... but I was very much in doubt about deadlock detection support... However, there seems to be a DeadlockCondition in the source and we have tests labelled Deadlock-.... So I guess deadlock detection works :)