PV1 ⊧ CLEARchecks a labelled transition system and visualises its problematic part

framework for debugging of concurrent systems

Application domain/field

• Model checking
• Debugging
• Concurrent systems

Type of tool

Debugging tool

Expected input

• LTS (Labelled Transition System)
• Property (MCL logic)

Format:

• LTS: AUT format
• Property: MCL logic

Expected output

• 3D Visual rendering: provides support for visualising the erroneous part of the LTS
• Abstraction techniques results: provides support to simplify counterexamples produced from the LTS and a given property