AirplaneLD and the semantics of colored net unfolding

View previous topic View next topic Go down

AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Sun 2 Apr - 19:32


Silvano again,

Always here to keep this forum alive.

I have some questions about the model AirplaneLD. I will consider the case N=10, but my issue affects all the cases.

The PDF description indicates that the model has 43,463 states and 183,664 transition firings (by the way, the PDF file has a bug for the size of the marking graphs for N=20). These are the results found by ITS and Marcie in 2016.

While I find the "right" number of reachable states, I only find 183,543 transitions. That is 121 less (keep this number in mind ;-))

Now, if we look at transition t3_2, it has condition [A >= 2000 OR A = 4000]. That is, once instantiated for N = 10, a condition of the form [A >= Altitude10 OR A = Altitude20].
Obviously, condition A = 4000 is superfluous. Moreover, in the case N = 10, transition t3_2 occurs 121 times in the reachability graph.

Conclusion, I think that the unfolding used by Marcie and ITS generate two occurrences of transition t3_2 for the case A = Altitude20; one for each sub-condition. I do not think that this should be the right semantics.

Any opinion of the organizers on this ?

PS: for the

Silvano

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by Admin on Wed 5 Apr - 20:42

Question... can you please precise the bug for N=20? I am ready to correct it (maybe you can confirm this is a cut/past problem between the number of nodes and the number of transitions ;-).

Concerning your remark about the difference in termes of transitions in the RG, it is of interest and I will push it to the authors of these tools. IN fact, they use different implementations of DD and, as far as I know, if Marcie has an unfolder in, ITS does not... to be clearer, do you work on the colored version?

Admin
Admin

Posts : 24
Join date : 2016-11-26

View user profile http://mc-contest.forumactif.com

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Wed 5 Apr - 23:12


Yes, I work with colored model, and I have some reasons to believe that my interpretation of "the problem" is correct.

If you take a colored model with a transition, say t, with a condition of the form (A or (A and A)) then you will have three transitions corresponding to t in the state graph for every state where t can fire (and A is true).

It should be easy to build a PNML file to test this hypothesis. I will try to do this tomorrow.

Said differently, if you change your Boolean condition with an "equivalent" one, then you can have more or less transitions than in the initial model. Equivalence of Boolean conditions does not preserve bisimulation, except if you define equivalence on formulas as syntactic equality !

Now, to be clear, I do not expect that tool authors adapt their tools to take this phenomenon into account. I have mentioned this issue because it stresses one of the problem with the colored models, meaning that the only available semantics derives from a tool (and how can I install it!) and not from a formal definition.

To conclude, I also think that it is curious to have a condition of the form (A >= 2000) or (A = 4000). This is not a bug, just something odd. Why not change the condition on the stripped models and see what happens.

Silvano

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Wed 5 Apr - 23:33


typo on the file http://mcc.lip6.fr/pdf/AirplaneLD-form.pdf

page 3, second line of the table (case N = 20), the number of transitions is 1.3391E+0006 and not 308303. You copied the value for the number of states.

Actually, we find:
N = 20, 308303 state(s), 1338663 transitions(s)

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by Admin on Thu 6 Apr - 9:11

Thank for the confirmation. This is corrected on our repository and should be propagated soon on the rest of the system.

Thank you.

Admin
Admin

Posts : 24
Join date : 2016-11-26

View user profile http://mc-contest.forumactif.com

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by crohr on Thu 6 Apr - 10:03

Hi,

as previously stated, Marcie unfolds any colored model and constructs the state space from it.
In this case and in any other cases Marcie's unfolded net is equivalent to the provided PT.

Did you find the parallel transition in the provided PT model?

Christian

crohr

Posts : 3
Join date : 2017-02-07

View user profile

Back to top Go down

its tools

Post by YannTM on Thu 6 Apr - 12:43

Hi,

Regarding its-tools : we do our own unfolding of the net, trying to respect the ISO standard for HLPN part 2. There is an ISO standard what you say " meaning that the only available semantics derives from a tool (and how can I install it!) and not from a formal definition." is wrong.

However, concerning number of edges in the graph, we disagree with other Tools on how it should be computed. As I've been defending for some time, the "correct" measure in my eyes is to count how many elements of SxS are in the relation. This means we have a set of edges, without duplicates.

This is what ITS-Tools was computing last year, see forum discussion on that from last year :
(CANNOT POST LINK !!)
(https:)

groups.google.com/forum/

#!topic/model-checking-contest-discussion-forum/AeWzL7Ry0TU

It indeed poses issues that the "translation" for analysis of CPN cannot do basic optimizations such as fusing bindings with identical effects, because the naïve translator used in the MCC does not do it.

For all these reasons,last year I sumittedmy tool computing UNIQUE edges, and got a lower confidence score, since nobody followed me. I still did it, otherwise I get different TRANSITIONS metrix from COL vs the same net in PT (due to optimizations/suppression of redundancy in the "unfolding process").

So, with my semantics,
a) what you describe is not possible, I'm not getting several occurrences due to translation artifacts
b) if you don't have the same edge count, probably you don't have the right graph/Kripke

As shown in the other forum posting, Dekker is a good example of multiple transitions getting fused.
But you can find many others, just look at last year detailed results, anywhere ITS-tools is getting RED in StateSpace on transition count is an occurrence of this (poorly designed, redundant models...).

Concerning the example itself, I think you are missing that the Altitude type is not a subset of integer, the "ordering" relation is poor.
So the MAX altitude is used to designate that the sensor is returning BAD values, it is thus distinguished in the net annotations (you can read it as  : we know the altitude is at least 20 or the altimeter is broken.

This is logically/business wise relevant.
Anyway, models are what they are, the MCC team only patches actual bugs in models (it has happened in the past).

Regards

yann

YannTM

Posts : 7
Join date : 2017-04-06

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Thu 6 Apr - 14:28

Yann,

Thanks for the pointers. I see that we agree on many things.

I was not aware that the ISO standards for PNML defined the semantics of unfolding in a tool-agnostic way. On the other hand, part 1 of the standard is 158 CHF on the ISO web page (!) this is why I have not read it. This is also why I have been asking for a reference to a paper or a research report that defines what is the unfolding of a high-level symmetric net. Tools submitters should have access to documentation that is not locked behind a paywall.

Actually I could be OK with your definition of "transitions count". Maybe a drawback is that it favors tools that do not really compute the transition relation, but for challenge 1 it seems a reasonable choice. Also, a good definition should give the "right" result when the colored Petri net is an ordinary Petri net, that is when all conditions are True and the only type is Dot. It does not seem to be the case with your proposal.

I agree that this is a very technical issue and I did not meant to imply that I am the only depository of the "truth" in this matter. I do not say that my definition should be adopted by everybody (I think I was clear about this in my posts).  My main concerns is to have an accepted definition of what should be the right number of transitions, and I would like that definition to be "tool-neutral". This is a problem only with high-level nets, I think that the answer for ordinary Petri nets is settled by the fact that we have a semantics "on paper". Anyway, thanks to this debate, I have a better understanding of what is expected and I will patch my tools accordingly.

Silvano

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Thu 6 Apr - 21:41


I have made available a very small PNML file, 1 state (of type process, an enumeration place), 1 place (with condition (x == 0) OR ((x == 0) AND (x == 0)) and one edge with "pattern" <x>

The reachability graph should have two states and two transitions with CPN-AMI; only one transition with Yann's semantics.

My goal is to have small examples that could be used as documentation or regression test for the use of high-level net.

The file is in a shared owncloud server in our lab: https: // cloud.laas.fr/index.php/s/h3zDmvSIUSvp3Jn

I have added a new option to my tool (-MCC) that adds the redundant transitions and that give the "expected" results. New version of the tool are also available in the same directory.

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Fri 7 Apr - 11:44


I have finally had the time to test with marcie and andl_converter (sorry, I have had to find a server with Ubuntu 16.04).

After converting the PNML example with andl_converter, Marcie finds 2 states and only 1 transition! so I will need to find a more elaborate example to test my theory.

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by amparore on Fri 7 Apr - 13:14

Dear Silvano,
   your net  "bisim.pnml" has correctly a single transition firing and 2 markings, because there exists a single colored variable binding [x=Process0] for which transition "main" can fire. I confirm with my tools that it has 2 markings and just one transition firing.

If you want to test a PNML model for your hypotesis on transition firings, use the one at the end of this post, which should have 2 markings ( m0=<P0=1,P1=0>   and m1=<P0=0,P1=1> )  and 2 transition firings (m0--[T0]-->m1  and m0--[T1]-->m1).

By the way. I think that there is no ambiguity on what is asked for the MCC.
Page 8 of the READ_ME.pdf asks for the number of transitions firings in the marking graph,
which is not the number of edges in the SxS relation, but the edges in the SxTxS relation.
The number of transitions firings in the marking graph is a standard concept for Petri nets, where the firing of a transition m0--[T0]--> m1  is not the same thing as the firing of another transition m0--[T1]--> m1.

Maybe Fabrice may clarify the topic for everyone.

Regards
--Elvio


----------------------------------------------------------
<?xml version="1.0"?>
<pnml xmlns="http://www.pnml.org/version-2009/grammar/pnml">
<net id="2markings_2firings" type="http://www.pnml.org/version-2009/grammar/ptnet">
<name>
<text>2markings_2firings</text>
</name>
<page id="page0">
<name>
<text>DefaultPage</text>
</name>
<!-- List of places -->
<place id="P0">
<name>
<graphics>
<offset x="0" y="15"/>
</graphics>
<text>P0</text>
</name>
<graphics>
<position x="100" y="100"/>
</graphics>
<initialMarking>
<text>1</text>
</initialMarking>
</place>
<place id="P1">
<name>
<graphics>
<offset x="0" y="15"/>
</graphics>
<text>P1</text>
</name>
<graphics>
<position x="220" y="100"/>
</graphics>
</place>
<!-- List of transitions -->
<transition id="T0">
<name>
<graphics>
<offset x="0" y="-15"/>
</graphics>
<text>T0</text>
</name>
<graphics>
<position x="165" y="70"/>
</graphics>
</transition>
<transition id="T1">
<name>
<graphics>
<offset x="0" y="-15"/>
</graphics>
<text>T1</text>
</name>
<graphics>
<position x="165" y="130"/>
</graphics>
</transition>
<!-- List of arcs -->
<arc id="id1" source="P0" target="T0">
</arc>
<arc id="id2" source="T0" target="P1">
</arc>
<arc id="id3" source="P0" target="T1">
</arc>
<arc id="id4" source="T1" target="P1">
</arc>
</page>
</net>
</pnml>

amparore

Posts : 4
Join date : 2016-11-30

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by YannTM on Fri 7 Apr - 17:44

Dear Elvio,

Just to clarify :"
Page 8 of the READ_ME.pdf asks for the number of transitions firings in the marking graph,
which is not the number of edges in the SxS relation, but the edges in the SxTxS relation.
The number of transitions firings in the marking graph is a standard concept for Petri nets, where the firing of a transition m0--[T0]--> m1  is not the same thing as the firing of another transition m0--[T1]--> m1.
"

Hem, except if the transition is a COLORED transition, and not a firing mode for the transition (bindings), you could very well fuse some of these event occurrences.
This is the whole issue, since the models are given in COLORED format, it is not obvious what the "T" you add to label the edges of the marking graph refers to.

Given that we do NOT have logic predicates in the MCC, allowing to distinguish  m0--[T0]--> m1  from m0--[T1]--> m1,
I don't see how you can claim so brazenly they are "not the same thing".

We are limited to Kripke Semantics currently (NO EVENT BASED LOGIC !!), and this despite the logic being pretty rich in atomic proposition types.

So this "marking graph" object is very poorly defined within the contest (w.r.t the Kripke, we have enough logic predicates to make sure all the Kripke the constestants are building are equivalent),
and the only reason to build it from a practical standpoint within the MCC contest, is to answer this sole metric "TRANSITIONS".

In any case, asking that COLORED and PT coincide on this metric is really taking things too far in my opinion, or just remove the colored models already if we can't take advantage of the colors being there.
Or extend the logic with events, and in that case it's legitimate to ask for that particular metric within the contest (and we would have an answer to whether bindings are part of the transition label or not).

I'll take the negative points/confidence score hit, rather than change my tool (killing structural reductions and simplifications ??) to compute such an irrelevant "Marking graph classical artifact style TRANSITIONS count".

In many cases (models crafted with more care) both coincide anyway,

Note that there IS NO business motivation to build redundant transitions in a Petri net, I've never seen one designed with that particular feature on purpose (please provide counter-examples if you have any).

Those that exist in the MCC should be mostly modeling artifacts (such as generated models, or translated models e.g. from color by a POOR/NAIVE translator).

Just my 2 cents, but if I convince enough participants I can get a consensus going maybe. Discussing with the organizers has proved sterile.

YannTM

Posts : 7
Join date : 2017-04-06

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by dalzilio on Fri 7 Apr - 18:26


Thank you all for the discussion.

With your help (especially thank to Yann for his trace on the DotandBoxes example), I have been able to better understand what is the expected number of transitions for colored models.

I see that now there is more than 2 available tools to 'compute' unfolding, andl_converter, Elvio's one (I don't know if it is available), mine (if it ever escapes from beta).

I will make available my latest version of my tool at the usual place later today: https: // cloud.laas.fr/index.php/s/h3zDmvSIUSvp3Jn

Maybe we could try to find a suitable format to compare results and avoid problems with future surprise models.

Silvano

dalzilio

Posts : 31
Join date : 2017-03-29

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by amparore on Fri 7 Apr - 22:00

Dear Yann
  I am not sure why you are using such strong words, but IMHO if you ask to count for transition firings, it is not equivalent to ask for the SxS cardinality.


Hem, except if the transition is a COLORED transition, and not a firing mode for the transition (bindings), you could very well fuse some of these event occurrences.
This is the whole issue, since the models are given in COLORED format, it is not obvious what the "T" you add to label the edges of the marking graph refers to.

Ah, now I understand your point...
But for what I know, the firing should include the binding. Consider, for instance, the paper:
"A symbolic reachability graph for coloured Petri nets", Chiola, Dutheillet, Franceschinis, Haddad.
where it is written, page 4:
"Using the firing rule, it is possible to construct a reachability graph, whose nodes
are the markings obtained from the initial marking by firing one or more transitions.
An arc between two markings is labeled by the name of the transition and the colour
whose firing determines the marking change. "


which, in my understanding, distinguishes transition firings through labeled edges (i.e. SxTxS), with the explicit clarification that T = <transition name> + <color bindings>.
Which implies that the transition firings in the colored Petri net are equivalent to their unfolding, since you will have an unfolded transition for every unique <transition name>*<binding> pair.

Our tool computes transition firings following the above definition. I don't pretend to claim that it is the only correct answer, but I think it is the "usual" definition of transition firing for Petri nets.
Anyway, I am interested in understanding if this will be the right semantics for this year contests, otherwise I will need to make changes or suppress the output before the submission.


We are limited to Kripke Semantics currently (NO EVENT BASED LOGIC !!), and this despite the logic being pretty rich in atomic proposition types.
I don't understand this point. I have not found any place in the MCC manual/site where it is claimed that we are restricted to the Kripke semantics. IMHO, Petri nets are defined on a more elaborate semantics than Kripke. Otherwise, even asking for "transition firings", or "tokens in place" does not make much sense in Kripke semantics, because there is no such thing as a "transition firing" or a "place token" in that semantics.

But your are surely right in pointing out that the overall semantics is under-defined, leaving space for corner-case misunderstandings.


===
Dear Silvano,
   if you are interested, you may find my unfolding here: GreatSPN Editor Homepage
Unfortunately, the scriptable interface converts&unfolds PNMLs into our own internal format, which is probably of very little value for you. But you may still use the graphical interface, which imports/exports the PNML format in P/T and Symmetric Net variations, which could be useful for you to experiment.

To unfold a PNML model, do this:
File->New  to create a new project
File->Import...->PNML file   imports the PNML net in the GUI
You will find the unfolding command in the toolbar, the last icon (a box that unfolds)
File->Export... -> PNML format   saves again in PNML.

However, consider that many PNML files included in the MCC set have been stripped of their graphical metadata, so you will have a blob of places/transitions collapsed together when you open them.
Last but not least, in the gui you cannot ask for a successor/predecessor on a color that does not belong to a circular class.


Regards.

--Elvio

amparore

Posts : 4
Join date : 2016-11-30

View user profile

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by Admin on Sat 8 Apr - 19:25

dalzilio wrote:
I see that now there is more than 2 available tools to 'compute' unfolding, andl_converter, Elvio's one (I don't know if it is available), mine (if it ever escapes from beta).

Emmanuel Paviot-Adet has developed on, and then, later, another one with Alban Linard. They are not working directly on PNML but I guess sources are available.

Best regards.

Admin
Admin

Posts : 24
Join date : 2016-11-26

View user profile http://mc-contest.forumactif.com

Back to top Go down

Re: AirplaneLD and the semantics of colored net unfolding

Post by Sponsored content


Sponsored content


Back to top Go down

View previous topic View next topic Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum