Skip to content

Instantly share code, notes, and snippets.

@wenjianhn
Created July 14, 2015 03:06
Show Gist options
  • Save wenjianhn/9ecf44f5f162187c1425 to your computer and use it in GitHub Desktop.
Save wenjianhn/9ecf44f5f162187c1425 to your computer and use it in GitHub Desktop.
Prove (x + y) % 3 = 0 => (10*x + y) % 3 = 0
---------------------------- MODULE DivideByThree ----------------------------
EXTENDS Integers
VARIABLES x, y
vars == <<x, y>>
Init == /\ x \in 1..9
/\ y \in 0..9
Next == \//\ x' = x + 1
/\ x' < 10
/\ UNCHANGED <<y>>
\//\ y' = y + 1
/\ y' < 10
/\ UNCHANGED <<x>>
\* TLC considers a reachable state from which there is no next
\* state satisfying the next-state action to be a deadlock error.
\* Termination is the deadlock that we want to happen. We need to
\* tell TLC to ignore deadlock by unchecking the Deadlock box in the What
\* to check section of the model overview page.
TypeOK == (x + y) % 3 = 0 => (10*x + y) % 3 = 0
Spec == Init /\ [][Next]_vars
=============================================================================
\* Modification History
\* Last modified Tue Jul 14 10:43:38 CST 2015 by jian
\* Created Tue Jul 14 10:07:49 CST 2015 by jian
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment