129 lines
3.1 KiB
Alloy
129 lines
3.1 KiB
Alloy
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]
|
|
}*/
|