adding German cache model

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