Authoritative location of known models and problem with DatabaseWithMutex-COL
3 posters
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1
Authoritative location of known models and problem with DatabaseWithMutex-COL
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 ?
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
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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.
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.
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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
Fabrice
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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
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
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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
Re: Authoritative location of known models and problem with DatabaseWithMutex-COL
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.
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.
Similar topics
» colored models; questions about Symmetric Nets and PNML
» Issue with NUPN .pnml definition in models provided for MCC2019
» Issue with NUPN .pnml definition in models provided for MCC2019
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum