Introduction

You will find below the correctness mask deduced from the analysis of tools outputs:

State Space Category

• StateSpace

Reachability Analysis Category

• ReachabilityComputeBounds
• ReachabilityBounds
• ReachabilityDeadlock
• ReachabilityCardinality
• ReachabilityFireabilitySimple
• ReachabilityFireability

CTL Category

• CTLCardinality
• CTLFireabilitySimple
• CTLFireability

LTL Category

• LTLCardinality
• LTLFireabilitySimple (no tool participated for any model)
• LTLFireability (no tool participated for any model)