From 39c9b6480bc9c09b399f54bd331f6110f3627df1 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 6 May 2016 17:02:01 +0200
Subject: [PATCH] Enforce monotonicity
---
randmu.py | 85 ++++++++++++++-----------------------------------------
1 file changed, 21 insertions(+), 64 deletions(-)
diff --git a/randmu.py b/randmu.py
index 2c1ed65..2494a11 100755
--- a/randmu.py
+++ b/randmu.py
@@ -61,15 +61,9 @@ class And(Propositional):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._left, Variable):
- self._left.finalize(atoms, guarded, unguarded, fixpoint)
- else:
- self._left = random.choice(atoms + guarded)
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
- if not isinstance(self._right, Variable):
- self._right.finalize(atoms, guarded, unguarded, fixpoint)
- else:
- self._right = random.choice(atoms + guarded)
class Or(Propositional):
@@ -93,38 +87,8 @@ class Or(Propositional):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._left, Variable):
- self._left.finalize(atoms, guarded, unguarded, fixpoint)
- else:
- self._left = random.choice(atoms + guarded)
-
- if not isinstance(self._right, Variable):
- self._right.finalize(atoms, guarded, unguarded, fixpoint)
- else:
- self._right = random.choice(atoms + guarded)
-
-
-
-class Not(Propositional):
- def __init__(self):
- self._subformula = Variable(self)
-
-
- def __str__(self):
- subformula = str(self._subformula)
- return "~(%s)" % (subformula,)
-
-
- def replace(self, what, withw):
- assert self._subformula == what
- self._subformula = withw
-
-
- def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._subformula, Variable):
- self._subformula.finalize(atoms, guarded, unguarded, fixpoint)
- else:
- self._subformula = random.choice(atoms + guarded)
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
@@ -148,10 +112,7 @@ class Box(Modal):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._subformula, Variable):
- self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
- else:
- self._subformula = random.choice(atoms + guarded)
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
@@ -171,10 +132,7 @@ class Diamond(Modal):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._subformula, Variable):
- self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
- else:
- self._subformula = random.choice(atoms + guarded)
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
@@ -201,14 +159,11 @@ class Mu(Fixpoint):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._subformula, Variable):
- if fixpoint == 'nu':
- guarded = []
- unguarded = []
+ if fixpoint == 'nu':
+ guarded = []
+ unguarded = []
- self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
- else:
- self._subformula = random.choice(atoms + guarded)
+ self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
@@ -232,18 +187,15 @@ class Nu(Fixpoint):
def finalize(self, atoms, guarded, unguarded, fixpoint):
- if not isinstance(self._subformula, Variable):
- if fixpoint == 'mu':
- guarded = []
- unguarded = []
+ if fixpoint == 'mu':
+ guarded = []
+ unguarded = []
- self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
- else:
- self._subformula = random.choice(atoms + guarded)
+ self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
-connectives = [And, And, Or, Or, Not, Box, Diamond, Mu, Nu]
+connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
class Variable:
@@ -264,7 +216,12 @@ class Variable:
def finalize(self, atoms, guarded, unguarded, fixpoint):
- assert False
+ choice = random.choice(guarded + atoms)
+ if choice in atoms:
+ choice = random.choice([choice, "~%s" % choice])
+
+ variables.remove(self)
+ self._parent.replace(self, choice)
--
GitLab