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

Please find enclosed the brute results for the CTLFireability 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 cc cc cc cc TFTFFFFT cc
005 cc cc cc cc FFFFFFFF cc
010 cc cc cc cc FFTFFFTF cc
020 cc cc cc cc to cc
050 cc cc cc cc cc cc
100 cc cc cc cc cc cc
200 cc cc cc cc cc cc
500 cc cc cc cc to cc
IBMB2S565S3960 (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none F-FT-F-F F-FT-F-F F-FT-F-F T-TT-T-T to cc
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 FFTTFFFT cc
06 cc cc cc cc FFFTFTTF cc
10 cc cc cc cc to cc
18 cc cc cc cc to cc
22 cc cc cc cc cc cc
28 cc cc cc cc cc cc
32 cc cc cc cc cc cc
Vasy2003 (P/T)
instances lola lola optimistic lola optimistic incomplete lola pessimistic marcie sara
none -T------ -T------ -T------ to FTFTTFFF -TT-T---