From ab0ccf6f0b6baa3155151a18b21f200f2b49fd42 Mon Sep 17 00:00:00 2001
From: Ken McMillan <myemail@thing.com>
Date: Tue, 2 Jan 2018 10:27:08 -0800
Subject: [PATCH] adding German cache model

---
 test/ibm-cache-N.ivy | 120 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 120 insertions(+)
 create mode 100644 test/ibm-cache-N.ivy

diff --git a/test/ibm-cache-N.ivy b/test/ibm-cache-N.ivy
new file mode 100644
index 0000000..55711f2
--- /dev/null
+++ b/test/ibm-cache-N.ivy
@@ -0,0 +1,120 @@
+#lang ivy1.7
+
+type client
+
+type message1 = { empty1 , reqshared , reqexclusive }
+
+type message2_4 = { empty2_4 , invalidate , grantshared , grantexclusive }
+
+type message3 = { empty3 , invalidateAck }
+
+type cachestate = { invalid , shared , exclusive }
+
+object s = {
+    var channel1(C:client) : message1
+    var channel2_4(C:client) : message2_4
+    var channel3(C:client) : message3
+    var cache(C:client) : cachestate
+    var homeSharerList(C:client) : bool
+    var homeinvalidateList(C:client) : bool
+    var homeexclusiveGranted : bool
+    var homeCurrentCommand : message1
+    var homeCurrentclient : client
+}
+
+var owner : client
+
+after init {
+    s.channel1(C) := empty1;
+    s.channel2_4(C) := empty2_4;
+    s.channel3(C) := empty3;
+    s.cache(C) := invalid;
+    s.homeSharerList(C) := false;
+    s.homeinvalidateList(C) := false;
+    s.homeexclusiveGranted := false;
+    s.homeCurrentCommand := empty1;
+}
+
+action reqsharedRule(cl:client) = {
+    require s.cache(cl) = invalid & s.channel1(cl) = empty1;
+    s.channel1(cl) := reqshared;
+}
+
+action reqexclusiveRule(cl:client) = {
+    require (s.cache(cl) = invalid | s.cache(cl) = shared) & s.channel1(cl) = empty1;
+    s.channel1(cl) := reqexclusive;
+}
+
+action pickNewRequestRule(cl:client) = {
+    require s.homeCurrentCommand = empty1 & s.channel1(cl) ~= empty1;
+    s.homeCurrentCommand := s.channel1(cl);
+    s.channel1(cl) := empty1;
+    s.homeCurrentclient := cl;
+    s.homeinvalidateList(C) := s.homeSharerList(C);
+}
+
+action sendinvalidateRule(cl:client) = {
+    require s.channel2_4(cl) = empty2_4 & s.homeinvalidateList(cl)
+    & (s.homeCurrentCommand = reqexclusive
+    | (s.homeCurrentCommand = reqshared & s.homeexclusiveGranted));
+    s.channel2_4(cl) := invalidate;
+    s.homeinvalidateList(cl) := false;
+}
+
+
+action receiveinvalidateAckRule(cl:client) = {
+    require s.homeCurrentCommand ~= empty1 & s.channel3(cl) = invalidateAck;
+    s.homeSharerList(cl) := false;
+    s.homeexclusiveGranted := false;
+    s.channel3(cl) := empty3;
+}
+
+action sharerinvalidatescacheRule(cl:client) = {
+    require s.channel2_4(cl) = invalidate & s.channel3(cl) = empty3;
+    s.channel2_4(cl) := empty2_4;
+    s.channel3(cl) := invalidateAck;
+    s.cache(cl) := invalid;
+}
+
+action receivesharedGrantRule(cl:client) = {
+    require s.channel2_4(cl) = grantshared;
+    s.cache(cl) := shared;
+    s.channel2_4(cl) := empty2_4;
+}
+
+action receiveexclusiveGrantRule(cl:client) = {
+    require s.channel2_4(cl) = grantexclusive;
+    s.cache(cl) := exclusive;
+    s.channel2_4(cl) := empty2_4;
+}
+
+action grantsharedRule = {
+    require s.homeCurrentCommand = reqshared
+    & ~ s.homeexclusiveGranted
+    & s.channel2_4(s.homeCurrentclient) = empty2_4;
+    s.homeSharerList(s.homeCurrentclient) := true;
+    s.homeCurrentCommand := empty1;
+    s.channel2_4(s.homeCurrentclient) := grantshared;
+}
+
+action grantexclusiveRule = {
+    require s.homeCurrentCommand = reqexclusive
+    & s.channel2_4(s.homeCurrentclient) = empty2_4 &
+    forall I. ~s.homeSharerList(I);
+    s.homeSharerList(s.homeCurrentclient) := true;
+    s.homeCurrentCommand := empty1;
+    s.homeexclusiveGranted := true;
+    s.channel2_4(s.homeCurrentclient) := grantexclusive;
+    owner := s.homeCurrentclient; 
+}
+
+
+
+invariant forall C1, C2. C1 ~= C2 & s.cache(C1) = exclusive -> s.cache(C2) = invalid
+
+invariant s.homeexclusiveGranted & s.homeCurrentCommand ~= empty1 & s.channel3(C1) = invalidateAck -> C1 = owner
+
+export reqsharedRule
+export reqexclusiveRule
+export pickNewRequestRule
+export receiveexclusiveGrantRule