Skip to content

Instantly share code, notes, and snippets.

@mdmarek

mdmarek/GCD.tla

Created November 3, 2016 16:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mdmarek/269d97c9e0b556efccf4bf0768fcbb09 to your computer and use it in GitHub Desktop.
Save mdmarek/269d97c9e0b556efccf4bf0768fcbb09 to your computer and use it in GitHub Desktop.
Download ZIP
TLA+ GCD
Raw
GCD.tla
---- MODULE GCD ----
EXTENDS Integers, TLC
Divides(p, n) == \E q \in -1000..1000 : n = q * p
DivisorsOf(n) == {p \in -1000..1000 : Divides(p, n)}
SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j
GCD(n, m) == SetMax(DivisorsOf(n) \cap DivisorsOf(m))
ASSUME PrintT(GCD(10,5))
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment