Start alloy spec

alloy/gcdt.als

@@ -0,0 +1,128 @@
+module gcdt[Operand]
+
+-- Top-level GCDT signature:
+sig GCDT {
+	-- A domain of operands
+	operand: Operand,
+
+	-- A universe of possible operations
+	ops: set Operation,
+
+	-- Sub-universe of commutative ops:
+	cOps: CommutativeOp & ops,
+
+	-- Sub-universe of pseudo-commutative ops:
+	pcOps: PseudoCommutativeOp & ops
+} {
+	ops = cOps + pcOps
+}
+
+
+
+-- All operations over GCDT's are binary:
+abstract sig Operation {
+	op: Operand one->one (Operand one->one Operand)
+}
+
+-- All operations should reflexively commute:
+fact commutes {
+	all opr: Operation | all opd1, opd2: Operand |
+		opr.op[opd1][opd2] = opr.op[opd2][opd1]
+}
+
+
+
+-- Commutative operations:
+sig CommutativeOp extends Operation {}
+
+-- Commutative operations distribute trivially:
+fact distributes {
+	all cop1, cop2: CommutativeOp | all op1, op2, op3: Operand |
+		cop1.op[cop2.op[op1][op2], op3] = cop1.op[op1, cop2.op[op2][op3]]
+}
+
+
+
+-- Pseudo-commutative operations:
+sig PseudoCommutativeOp extends Operation {
+	right: Operand
+}
+
+-- Pseudo-commutative operations fold into subsequent operands:
+fact pseudoCommutes {
+	all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
+	all opd1, opd2, opd3, opd4: Operand |
+		pop.op[cop1.op[cop2.op[opd1, opd2], opd3], opd4] =
+			cop1.op[cop2.op[pop.op[opd1, opd4], pop.op[opd2, opd4]], pop.op[opd3, opd4]]
+}
+
+
+
+-- A single operation applied to a GCDT:
+sig GCDTDiff {
+	op: one Operation,
+	right: one Operand
+}
+
+
+-- An order-agnostic set of operations applied to a GCDT:
+sig GCDTBatch {
+	type: one GCDT,
+	base: one Operand,
+	ops: set GCDTDiff,
+	fold: Operand one->one Operand
+} {
+	base in type.operand
+	ops = {diff: ops | diff.op in type.ops && diff.right in type.operand}
+}
+
+
+fun applyDiff [diff: GCDTDiff, opd: Operand]: Operand {
+	diff.op.op[opd][diff.right]
+}
+
+run applyDiff for 4
+
+fun composeFold [opr: one Operation, right: one Operand, fold: Operand one->one Operand]: Operand one->one Operand {
+	{lhs, rhs: Operand | rhs = fold[opr.op[lhs][right]] }
+}
+
+pred batchStep [batch1, batch2: GCDTBatch, diff: one GCDTDiff] {
+	diff in batch1.ops
+	batch1.type = batch2.type
+	batch2.base = diff.op.op[batch1.fold[batch1.base]][batch1.fold[diff.right]]
+	(diff.op in batch1.type.pcOps) => batch2.fold = composeFold[diff.op, diff.right, batch1.fold]
+	else batch2.fold = batch1.fold
+	batch2.ops = batch1.ops - diff
+}
+
+run batchStep for 4
+
+fun batchSteps [] : GCDTBatch one->one GCDTBatch {
+	{ batch1, batch2 : GCDTBatch | some diff: GCDTDiff | batchStep[batch1, batch2, diff] }
+}
+
+run batchSteps for 4
+
+check batchCommutes2 : 
+
+/*pred batchOneStep[batch: one GCDTBatch, fold: Operand one->one Operand] {
+	result in batch.type.operand
+	batch = {diff: batch |
+		some val | val = diff.op.op[
+}*/
+
+-- This is wrong as it doesn't accumulate pseudo-commutative operations
+/*pred recApplyDiff [type: GCDT, batch: set GCDTDiff, inOpd, outOpd: Operand] {
+	inOpd in type.operand
+	outOpd in type.operand
+	batch = {diff: batch |
+		diff.op in type.ops
+		&& diff.right in type.operand
+		&& recApplyDiff[type, (batch - diff), applyDiff[type, diff, inOpd], outOpd]
+		&& outOpd in type.operand}
+}
+
+pred evalBatch [batch: one GCDTBatch, result: Operand] {
+	recApplyDiff[batch.type, batch.ops, batch.base, result]
+}*/