MCC'2013 - CTLFireability Scores

Please find enclosed the scores for the CTLFireability examination. We display only the score of tools that provide a results for at least one instance of one model. The total is first listed in the table below followed by a detail, for each proposed model. You may access the corresponding result page here

Meaning of the line labels are:

1st instance: the tool gets a bonus for having processed the first instance of this model (+1 point),
instances: the tool gets 1 point per instances treated (for that, we assume that at least one formula has been successfuly computed),
max reached: the tool could process all the instances for the model (+2 points),
best: the tool is among the ones that processed a maximum of instances within the time and memory confinement (+2 points).

For known, a tool may collect up to 411 points.

Total Score of the tools
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
Global Score	47	198	198	178	113	83	152
CSRepetitions (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
CSRepetitions (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	2	6	6	5	2	2	6
max reached	0	2	2	0	0	0	2
best	0	2	2	0	0	0	2
subtotal	3	11	11	6	3	3	11
Dekker (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	0
instances	0	5	5	5	3	2	0
max reached	0	0	0	0	0	0	0
best	0	2	2	2	0	0	0
subtotal	0	8	8	8	4	3	0
DotAndBoxes (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
DrinkVendingMachine (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
DrinkVendingMachine (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	0
instances	0	1	1	1	1	2	0
max reached	0	0	0	0	0	2	0
best	0	0	0	0	0	2	0
subtotal	0	2	2	2	2	7	0
Echo (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	0	1
instances	0	9	9	9	3	0	4
max reached	0	2	2	2	0	0	0
best	0	2	2	2	0	0	0
subtotal	0	14	14	14	4	0	5
Eratosthenes (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	1
instances	0	6	6	6	6	6	6
max reached	0	2	2	2	2	2	2
best	0	2	2	2	2	2	2
subtotal	0	11	11	11	11	11	11
FMS (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	6	8	8	8	7	3	8
max reached	0	2	2	2	2	0	2
best	0	2	2	2	2	0	2
subtotal	7	13	13	13	12	4	13
GlobalRessAlloc (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
GlobalRessAlloc (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	0	1	0
instances	1	1	1	1	0	1	0
max reached	0	0	0	0	0	0	0
best	2	2	2	2	0	2	0
subtotal	4	4	4	4	0	4	0
Kanban (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	5	8	8	8	5	2	8
max reached	0	2	2	2	2	0	2
best	0	2	2	2	2	0	2
subtotal	6	13	13	13	10	3	13
LamportFastMutEx (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
LamportFastMutEx (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	1	0
instances	0	0	0	0	0	2	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	2	0
subtotal	0	0	0	0	0	5	0
MAPK (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	2	6	6	6	4	3	5
max reached	0	2	2	2	0	0	2
best	0	2	2	2	0	0	2
subtotal	3	11	11	11	5	4	10
NeoElection (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
NeoElection (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	1
instances	0	4	4	3	2	1	7
max reached	0	0	0	0	0	0	2
best	0	0	0	0	0	0	2
subtotal	0	5	5	4	3	2	12
PermAdmissibility (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
PermAdmissibility (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	5	6	6	6	2	1	4
max reached	2	2	2	2	2	0	2
best	2	2	2	2	2	0	2
subtotal	10	11	11	11	7	2	9
Peterson (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
Peterson (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	0	1
instances	0	5	5	4	4	0	3
max reached	0	2	2	2	2	0	0
best	0	2	2	2	2	0	0
subtotal	0	10	10	9	9	0	4
Philosophers (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
Philosophers (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	3	11	11	11	4	1	6
max reached	0	2	2	2	0	0	0
best	0	2	2	2	0	0	0
subtotal	4	16	16	16	5	2	7
PhilosophersDyn (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
PhilosophersDyn (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	1
instances	2	2	2	2	2	1	2
max reached	0	0	0	0	0	0	0
best	2	2	2	2	2	0	2
subtotal	5	5	5	5	5	2	5
Planning (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
Railroad (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	0	1
instances	0	3	3	3	1	0	2
max reached	0	0	0	0	0	0	0
best	0	2	2	2	0	0	2
subtotal	0	6	6	6	2	0	5
RessAllocation (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	1
instances	0	14	14	12	11	12	12
max reached	0	0	0	0	0	0	2
best	0	0	0	0	0	0	2
subtotal	0	15	15	13	12	13	17
Ring (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	0	1	1
instances	0	1	1	1	0	1	1
max reached	0	2	2	2	0	2	2
best	0	2	2	2	0	2	2
subtotal	0	6	6	6	0	6	6
RwMutex (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	1
instances	0	12	12	10	9	4	12
max reached	0	2	2	2	0	0	2
best	0	2	2	2	0	0	2
subtotal	0	17	17	15	10	5	17
SharedMemory (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
SharedMemory (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	0	1
instances	2	5	5	2	2	0	3
max reached	0	0	0	0	0	0	0
best	0	2	2	0	0	0	0
subtotal	3	8	8	3	3	0	4
SimpleLoadBal (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
SimpleLoadBal (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	1	1	1	1	1	1
instances	0	4	4	3	3	1	2
max reached	0	0	0	0	0	0	0
best	0	2	2	2	0	0	0
subtotal	0	7	7	6	4	2	3
TokenRing (Colored)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	0	0	0	0	0	0	0
instances	0	0	0	0	0	0	0
max reached	0	0	0	0	0	0	0
best	0	0	0	0	0	0	0
subtotal	0	0	0	0	0	0	0
TokenRing (P/T)
	greatSPN	lola	lola optimistic	lola optimistic incomplete	lola pessimistic	marcie	sara
1st instance	1	1	1	1	1	1	0
instances	1	2	2	1	1	2	0
max reached	0	0	0	0	0	0	0
best	0	2	2	0	0	2	0
subtotal	2	5	5	2	2	5	0