fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Results for the CTLMarkingComparison Examination
Last Updated
Apr. 26, 2013

Please find enclosed the brute results for the CTLMarkingComparison examination. We display only the score of tools that provide a results for at least one instance of one model. You may access to the scoring for this examination here.

The legend for the values is provided below:

Note on the display of results for formulas: each formula is considered as a flag (F if false, T if true, - or ? when the value cannot be determined). These values are concatenated in the order they appear (we assume it is the order of formulas as they were provided).

HouseConstruction (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
002 nf nf nf nf nf nf
005 nf nf nf nf nf nf
010 nf nf nf nf nf nf
020 nf nf nf nf nf nf
050 nf nf nf nf nf nf
100 nf nf nf nf nf nf
200 nf nf nf nf nf nf
500 nf nf nf nf nf nf
IBMB2S565S3960 (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nf nf nf nf nf nf
QuasiCertifProtocol (Colored)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 nc nc nc nc nc nc
06 nc nc nc nc nc nc
10 nc nc nc nc nc nc
18 nc nc nc nc nc nc
22 nc nc nc nc nc nc
28 nc nc nc nc nc nc
32 nc nc nc nc nc nc
QuasiCertifProtocol (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
02 cc cc cc cc FFFFFFFF -----FF-
06 cc cc cc cc FFFFFFFF T-TTF--F
10 cc cc cc cc to ---T--T-
18 cc cc cc cc to -FT--T--
22 cc cc cc cc cc -FFF-T--
28 cc cc cc cc cc -FTF----
32 cc cc cc cc cc TT---TT-
Vasy2003 (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none nf nf nf nf nf nf