Forum for the Model Checking Contest
Would you like to react to this message? Create an account in a few clicks or log in to continue.

Authoritative location of known models and problem with DatabaseWithMutex-COL

3 posters

Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by dalzilio Wed 12 Apr - 11:32

Hello,

I have been working with PNML models coming from two different sources:

1/ files downloaded from the http://mcc.lip6.fr/models.php page, for instance http://mcc.lip6.fr/archives/DatabaseWithMutex-pnml.tar.gz for the DatabaseWithMutex examples.

2/ files extracted from the 2016 Submission Kit after applying the two existing patches (e.g. http://mcc.lip6.fr/2016/archives/MCC-INPUTS_MODIFIED-2.tgz). Models can be found in the INPUTS folder; each instances in a separate tgz archive.

I prefer the second source since it is closer (I think) to the real conditions of the competition.

My problem is that the PNML model for DatabaseWithMutex (COL instances) are very different between the two available sources. Actually, I think that the file in INPUTS/DatabaseWithMutex-COL-02.tgz is not valid PNML.

So my question are:

- what is the authoritative source for finding the known PNML models for 2017 ? (I know that the submission kit is due very soon)

- did anyone found problems with the DatabaseWithMutex-COL-* models of the 2016 competition ?

dalzilio

Posts : 31
Join date : 2017-03-29

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by Admin Wed 12 Apr - 17:35

I will let Lom answer this question (the is travelling). The archive from the 2016 submission you can take from any public VM is the one used last year (but the URL you mention should be good too). The "model page" only provides information model per model for information (and possibly another use) only.

However, both are generated from the same source by several scripts so they should be the same. Can you please point out the differences you notice on the smallest instance with a diff?

Apparently, no problem was found in 2016 (see there: http://mcc.lip6.fr/2016/index.php?CONTENT=results/StateSpace.html&TITLE=Results%20for%20StateSpace). ITS-Tool did not compute the same number of states than Marcie but the unfolding confirms Marcie should be right (and ITS-Tools finds the number of transitions in the P/T version... Maybe the interpretation problem Yann mentions in another thread.

Admin
Admin

Posts : 25
Join date : 2016-11-26

https://mc-contest.forumactif.com

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by dalzilio Wed 12 Apr - 18:04


Taken from file DatabaseWithMutex-COL-02/model.pnml.

MD5 hash of file DatabaseWithMutex-COL-02/model.pnml:
75 e3 71 36 16 14 3f 4b 37 b9 34 6a bc 59 42 ae

On the arc for transitions change to the place message (arc 35), line 237, I have the following expression that should corresponds to <text>1'[(site.all),(f)] - 1'[(s),(f)]</text>. I use a simplified XML syntax to be more readable:

subtract>
subterm>add>subterm>numberof> 1' , tuple>(site1, varf) , tuple>(site2,varf)
subterm>numberof>1' , tuple>(vars, varf)

So an add element with only one subterm (why not) encompassing a numberof with three subelements.

File DatabaseWithMutex-pnml/database2.pnml, taken form the models.php page on the MCC website, has instead something like:

MD5 hash of file DatabaseWithMutex-pnml/database2.pnml:
4f 9a 62 7a cb 00 ed c3 a3 b4 a9 ae 56 fa 8c 9a


subtract>
subterm>subterm>add>numberof> 1' , tuple>(site1, varf)
numberof> 1' , tuple>(site2,varf)
subterm>numberof>1' , tuple>(vars, varf)

dalzilio

Posts : 31
Join date : 2017-03-29

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by Admin Wed 12 Apr - 18:08

I had a look on the svn logs for this model. There was some changes done in April and May 2016 but none that should have affected the PNML. I push this to Lom.

Fabrice

Admin
Admin

Posts : 25
Join date : 2016-11-26

https://mc-contest.forumactif.com

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by lhillah Thu 13 Apr - 11:24

Hi,

Here is a link to download the latest version I found in our repository, from which the patched version of last year should have been produced.
https://cloud.lip6.fr/index.php/s/GDa1V97zHWtOWDS

In the mentioned annotation, I found a subtract element having two subterms: an add subterm (with the expanded 1'[(site.all), (f)] as subterms), and the tuple 1'[(s), (f)].

Can you please compare?

Best regards,
Lom


lhillah

Posts : 9
Join date : 2017-01-04

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by dalzilio Thu 13 Apr - 11:41


The MD5 hash confirms that the second PNML file I mention in my message is the same than in the archive you made available on the owncloud. If this will be the XML use for the file DatabaseWithMutex-COL-02/model.pnml in the 2017 BenchKit then I am relieved.

However, this file is different from what I have found in the INPUTS folder of the 2016 BenchKit (after applying the 2 patches cited in your webpages). Maybe I have missed a later patch, maybe some other file was used during the competition.

I just wanted to make sure of where I should find PNML files for the known examples ... if possible using conditions that are as close as possible to the real competitions, so that we can test our scripts in real conditions.

Silvano

dalzilio

Posts : 31
Join date : 2017-03-29

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by Admin Sun 16 Apr - 19:19

Do not worry, We will use the qualification phase to check for this. I just returned from vacation and I am preparing the patch with the models where bugs were mentioned.

By the way, you should have used the mcc-2017 VM that should contain the appropriate version of PNML since the correction was done before it was produced.

Admin
Admin

Posts : 25
Join date : 2016-11-26

https://mc-contest.forumactif.com

Back to top Go down

Authoritative location of known models and problem with DatabaseWithMutex-COL Empty Re: Authoritative location of known models and problem with DatabaseWithMutex-COL

Post by Sponsored content


Sponsored content


Back to top Go down

Back to top

- Similar topics

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