More tweaks to alloy theories

1 year ago · 718b88ac8c
parent 2da298cc0f
commit 718b88ac8c
2 changed files with 75 additions and 1 deletions
--- a/alloy/gcdt.als
+++ b/alloy/gcdt.als
@ -104,7 +104,34 @@ fun batchSteps [] : GCDTBatch one->one GCDTBatch {

 run batchSteps for 4

-check batchCommutes2 : 
+/*batchCommutes2: check {
+	some dt: GCDT | all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
+		all diff1, diff2, diff3: GCDTDiff | all opBase: Operand |
+		all batch1, batch2, batch3, batch4, batch5, batch6, batch7: GCDTBatch |
+		all batch8, batch9, batch10, batch11, batch12, batch13, batch14: GCDTBatch |
+			(dt.cOps = cop1 + cop2 && dt.pcOps = pop) =>
+			(diff1.op = cop1 && diff2.op = cop2 && diff3.op = pop) =>
+			(batch1.type = dt && batch1.base = opBase && batch1.fold = iden) =>
+			(batch1.ops = diff1 + diff2 + diff3) =>
+		 		   batchStep[batch1,  batch2,  diff1]
+				&& batchStep[batch2,  batch3,  diff2]
+				&& batchStep[batch3,  batch4,  diff3]
+				&& batchStep[batch1,  batch5,  diff1]
+				&& batchStep[batch5,  batch6,  diff3]
+				&& batchStep[batch6,  batch4,  diff2]
+				&& batchStep[batch1,  batch7,  diff2]
+				&& batchStep[batch7,  batch8,  diff1]
+				&& batchStep[batch8,  batch4,  diff3]
+				&& batchStep[batch1,  batch9,  diff2]
+				&& batchStep[batch9,  batch10, diff3]
+				&& batchStep[batch10, batch4,  diff1]
+				&& batchStep[batch1,  batch11, diff3]
+				&& batchStep[batch11, batch12, diff1]
+				&& batchStep[batch12, batch4,  diff2]
+				&& batchStep[batch1,  batch13, diff3]
+				&& batchStep[batch13, batch14, diff2]
+				&& batchStep[batch14, batch2,  diff1]  -- FIXME: this is wrong. Should be batch4 
+} for exactly 1 GCDT, 2 CommutativeOp, 1 PseudoCommutativeOp, 3 GCDTDiff, 6 Operand, 14 GCDTBatch

 /*pred batchOneStep[batch: one GCDTBatch, fold: Operand one->one Operand] {
 	result in batch.type.operand
--- a/alloy/gcdt_int.als
+++ b/alloy/gcdt_int.als
@ -0,0 +1,47 @@
+open util/integer
+open gcdt[Int]
+
+fun getPlus [n: Int]: Int one->one Int {
+	{lhs, rhs: Int | rhs = lhs + n}
+}
+
+fun getTimes [n: Int]: Int one->one Int {
+	{lhs, rhs: Int | rhs = mul[lhs][n]}
+}
+
+fun opPlus : CommutativeOp {
+	{cop : CommutativeOp | cop.op = getPlus }
+}
+
+fun opTimes [n: Int]: PseudoCommutativeOp {
+	{pcop : PseudoCommutativeOp | pcop.op = getTimes && pcop.right = n}
+}
+
+batchCommutes2: check {
+	some dt: GCDT | all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
+		all diff1, diff2, diff3: GCDTDiff | all opBase: Int |
+		all batch1, batch2, batch3, batch4/*, batch5, batch6, batch7*/: GCDTBatch |
+		//all batch8, batch9, batch10, batch11, batch12, batch13, batch14: GCDTBatch |
+			(dt.cOps = cop1 + cop2 && dt.pcOps = pop) =>
+			(diff1.op = cop1 && diff2.op = cop2 && diff3.op = pop) =>
+			(batch1.type = dt && batch1.base = opBase && batch1.fold = iden) =>
+			(batch1.ops = diff1 + diff2 + diff3) =>
+		 		   batchStep[batch1,  batch2,  diff1]
+				&& batchStep[batch2,  batch3,  diff2]
+				&& batchStep[batch3,  batch4,  diff3]
+				//&& batchStep[batch1,  batch5,  diff1]
+				//&& batchStep[batch5,  batch6,  diff3]
+				//&& batchStep[batch6,  batch4,  diff2]
+				//&& batchStep[batch1,  batch7,  diff2]
+				//&& batchStep[batch7,  batch8,  diff1]
+				//&& batchStep[batch8,  batch4,  diff3]
+				//&& batchStep[batch1,  batch9,  diff2]
+				//&& batchStep[batch9,  batch10, diff3]
+				//&& batchStep[batch10, batch4,  diff1]
+				//&& batchStep[batch1,  batch11, diff3]
+				//&& batchStep[batch11, batch12, diff1]
+				//&& batchStep[batch12, batch4,  diff2]
+				//&& batchStep[batch1,  batch13, diff3]
+				//&& batchStep[batch13, batch14, diff2]
+				//&& batchStep[batch14, batch2,  diff1]  -- FIXME: this is wrong. Should be batch4 
+} for exactly 1 GCDT, 2 CommutativeOp, 1 PseudoCommutativeOp, 3 GCDTDiff, 6 Int, 4 GCDTBatch