Guessing, Model Checking and Theorem Proving of State Machine Properties – A Case Study on Qlock

State Machine Graphical Animation (SMGA) tool 
1. a template picture of Mod3
2. a sequence of states for Mod3
3. a template picture of Qlock
4. a sequence of states for Qlock

Specification of Mod3 in Maude
Specification of Mod3 in CafeOBJ (incuding proof score)

Specification of Qlock in Maude
Specification of Qlock in CafeOBJ
Proof score for inv1
Proof score for inv2
Proof score for inv3
Proof score for inv4
Proof score for inv5
Proof score for inv6
Proof score for inv7