[procilege commit] r76 - in trunk/procilege/src: main/java/merisis/traitspace main/java/procilege/impl test/java/mer...
codesite...@google.com
Date: Mon Jun 11 07:09:56 2007
New Revision: 76
Added:
trunk/procilege/src/test/java/merisis/traitspace/MorphismProofTest.java
Modified:
trunk/procilege/src/main/java/merisis/traitspace/Morphism.java
trunk/procilege/src/main/java/procilege/impl/ComputationalEntityMgr.java
trunk/procilege/src/test/java/procilege/test/PrivilegeCongruentTest.java
trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest1.java
trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest2.java
Log:
[Issue 34]The proofness of morphism.
Modified: trunk/procilege/src/main/java/merisis/traitspace/Morphism.java
==============================================================================
--- trunk/procilege/src/main/java/merisis/traitspace/Morphism.java (original)
+++ trunk/procilege/src/main/java/merisis/traitspace/Morphism.java Mon Jun 11 07:09:56 2007
@@ -4,6 +4,7 @@
import static merisis.util.BitUtil.bitsetOrArray;
import java.util.ArrayList;
+import java.util.List;
import java.util.logging.Level;
import java.util.logging.Logger;
@@ -62,6 +63,78 @@
new OpenBitSet(), isRecursive));
}
+ /**
+ * Proof the implications.
+ *
+ * @param f
+ * the relation to be proofed
+ * @param a
+ * @param b
+ * @return
+ */
+ public boolean proof(long f, long[][] a, long[][] b) {
+
+ int numa = a.length;
+ int numb = b.length;
+
+ // reduce and group the implications.
+ ArrayList<long[]> diads = new ArrayList<long[]>();
+ List<List<Integer>> groups = new ArrayList<List<Integer>>();
+ for (int i = 0; i < numa; i++) {
+ long[] la = a[i];
+ for (int j = 0; j < numb; j++) {
+ long[] lb = b[i];
+
+ ArrayList<Integer> group = new ArrayList<Integer>();
+ for (int ia = 0; ia < la.length; ia++) {
+ for (int ib = 0; ib < lb.length; ib++) {
+
+ long[] diad = new long[] { la[ia], lb[ib] };
+ int index = diads.indexOf(diad);
+ if (index == -1) {
+
+ diads.add(diad);
+ group.add(diads.size() - 1);
+ } else {
+ group.add(index);
+ }
+ }
+ }
+ groups.add(group);
+ }
+ }
+
+ for (List<Integer> group : groups) {
+
+ boolean test = true;
+ for (int i : group) {
+
+ long[] diad = diads.get(i);
+
+ if (!exists(f, diad[0], diad[1])) {
+ test = false;
+
+ if (logger.isLoggable(Level.FINEST)) {
+ logger.finest(String.format(
+ "proofed %d: %d -> %d, FALSE", f, diad[0],
+ diad[1]));
+ }
+ break;
+ }
+
+ if (logger.isLoggable(Level.FINEST)) {
+ logger.finest(String.format("proofed %d: %d -> %d, TRUE",
+ f, diad[0], diad[1]));
+ }
+ }
+
+ if (test)
+ return true;
+ }
+
+ return false;
+ }
+
private OpenBitSet computeCodomain(long f, OpenBitSet todo,
OpenBitSet checked, OpenBitSet result, boolean isRecursive) {
@@ -206,14 +279,14 @@
} finally {
mvm.stepout();
}
-
+
long[] sp = mvm.read();
if (sp == null)
continue;
for (int j = 0; j < sp.length; j++) {
- mvm.give(f,b);
+ mvm.give(f, b);
mvm.source();
mvm.give(sp[j]);
mvm.focus();
@@ -234,7 +307,7 @@
} finally {
mvm.stepout();
}
-
+
long[] sp = mvm.read();
if (sp == null)
continue;
@@ -248,12 +321,11 @@
if (mvm.read() != null)
continue;
- suspInfimum.add(sp[j]);
+ suspInfimum.add(sp[j]);
}
}
-
- for(long witness : suspInfimum) {
+ for (long witness : suspInfimum) {
mvm.autobeam();
try {
@@ -262,12 +334,11 @@
} finally {
mvm.stepout();
}
-
+
long[] sp = mvm.read();
if (sp == null)
continue;
-
for (int j = 0; j < sp.length; j++) {
mvm.give(f);
@@ -277,12 +348,13 @@
if (mvm.read() != null)
continue;
- infimum.set(sp[j]);
+ infimum.set(sp[j]);
}
}
if (logger.isLoggable(Level.FINEST)) {
- logger.finest(String.format("a-infimum: {%s}", BitUtil.toString(infimum)));
+ logger.finest(String.format("a-infimum: {%s}", BitUtil
+ .toString(infimum)));
}
return infimum;
Modified: trunk/procilege/src/main/java/procilege/impl/ComputationalEntityMgr.java
==============================================================================
--- trunk/procilege/src/main/java/procilege/impl/ComputationalEntityMgr.java (original)
+++ trunk/procilege/src/main/java/procilege/impl/ComputationalEntityMgr.java Mon Jun 11 07:09:56 2007
@@ -55,13 +55,16 @@
private long nameIsA = 0;
- private boolean initial = true;
+ private boolean initialized = true;
public ComputationalEntityMgr() {
}
private void init() {
+
+ if (!initialized)
+ return;
namePalLiteral = smr.sense(new QName(PAL_METAENTITY_NS,
PAL_LITERAL_CONTENT));
@@ -72,13 +75,15 @@
namePropEntities = smr.sense(new QName(PROPS_NS, PROPS_ALLENTITYS));
nameIsA = smr.sense(new QName(PROPS_NS, RELATIONS_ISA));
-
- initial = false;
+
+ eh.ripple(new long[] {namePrivExpr}, PrivilegeFormReaction.class);
+
+ initialized = false;
}
public long updateContentOfPalLiteral(long threadfocus, String literal) {
- if (initial)
+ if (initialized)
init();
return 0;
@@ -86,7 +91,7 @@
public void updateLiteralContent(String content) {
- if (initial)
+ if (initialized)
init();
if (logger.isLoggable(Level.FINEST)) {
@@ -102,7 +107,7 @@
public void updatePrivlegeExpr(Name name, PrivExprElement expr) {
- if (initial)
+ if (initialized)
init();
mvm.give(((NameImpl) name).nameId);
@@ -118,7 +123,7 @@
public PrivExprElement retrievePrivlegeExpr(Name name) {
- if (initial)
+ if (initialized)
init();
Object value;
@@ -141,10 +146,10 @@
public PrivilegeForm retrievePrivlegeForm(Name name) {
- if (initial)
+ if (initialized)
init();
- if (initial)
+ if (initialized)
init();
Object value;
@@ -167,7 +172,7 @@
public void setEntityProperty(Name entity, String property, Object value) {
- if (initial)
+ if (initialized)
init();
mvm.give(((NameImpl) entity).nameId);
@@ -184,7 +189,7 @@
public Object getEntityProperty(Name entity, String property) {
- if (initial)
+ if (initialized)
init();
Object value;
Added: trunk/procilege/src/test/java/merisis/traitspace/MorphismProofTest.java
==============================================================================
--- (empty file)
+++ trunk/procilege/src/test/java/merisis/traitspace/MorphismProofTest.java Mon Jun 11 07:09:56 2007
@@ -0,0 +1,58 @@
+package merisis.traitspace;
+
+import static junit.framework.Assert.assertTrue;
+import junit.framework.Assert;
+
+import org.junit.Test;
+
+import com.google.inject.Inject;
+
+public class MorphismProofTest extends AbstractTraitSpaceTest {
+
+ @Inject
+ private Morphism mp;
+
+ @Test
+ public void case1() {
+
+ Assert.assertEquals(1, n("T0"));
+ Assert.assertEquals(2, n("isa"));
+ Assert.assertEquals(3, n("a"));
+ Assert.assertEquals(4, n("b"));
+ Assert.assertEquals(5, n("c"));
+ ht.emerge(n("T0"), n("a"));
+ ht.emerge(n("T0"), n("b"));
+ ht.emerge(n("T0"), n("c"));
+
+ long isa = n("isa");
+
+ mvm.give(n("T0"));
+ mvm.stepin();
+ try {
+
+ mp.set(isa, n("a"), n("b"));
+ mp.set(isa, n("b"), n("c"));
+ mp.set(isa, n("d"), n("b"));
+ mp.set(isa, n("d"), n("e"));
+
+ dumpHistory(0, 30);
+
+ // ? a -> c
+ assertTrue(mp.proof(isa, new long[][] { { n("a") } },
+ new long[][] { { n("c") } }));
+
+ // ? a -> ( c || e )
+ assertTrue(mp.proof(isa, //
+ new long[][] { { n("a") } }, //
+ new long[][] { { n("c") }, { n("e") } }));
+
+ // ? (a && d) -> ( c || e )
+ assertTrue(mp.proof(isa, //
+ new long[][] { { n("a"), n("d") } }, //
+ new long[][] { { n("c") }, { n("e") } }));
+
+ } finally {
+ mvm.stepout();
+ }
+ }
+}
\ No newline at end of file
Modified: trunk/procilege/src/test/java/procilege/test/PrivilegeCongruentTest.java
==============================================================================
--- trunk/procilege/src/test/java/procilege/test/PrivilegeCongruentTest.java (original)
+++ trunk/procilege/src/test/java/procilege/test/PrivilegeCongruentTest.java Mon Jun 11 07:09:56 2007
@@ -9,12 +9,13 @@
import procilege.lang.PrivExprMergence;
import procilege.lang.PrivilegeForm;
import procilege.lang.PrivilegeFormAnalysis;
+import procilege.test.pal.AbstractPalTest;
import com.google.inject.Guice;
import com.google.inject.Inject;
import com.google.inject.Injector;
-public class PrivilegeCongruentTest {
+public class PrivilegeCongruentTest extends AbstractPalTest {
@Test
public void checkCongruency() {
Modified: trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest1.java
==============================================================================
--- trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest1.java (original)
+++ trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest1.java Mon Jun 11 07:09:56 2007
@@ -16,23 +16,26 @@
@Test
public void test1() {
- mvm.give(nm("testcase"));
+ mvm.give(nm("T0"));
mvm.stepin();
+ try {
+ def(nn("p1"), pvm(nn("a")));
+ dumpHistory(0, 30);
+ assertEquals(pvm(nn("a")), cem.retrievePrivlegeExpr(nn("p1")));
- def(nn("p1"), pvm(nn("a")));
- dumpHistory(0, 30);
- assertEquals(pvm(nn("a")), cem.retrievePrivlegeExpr(nn("p1")));
+ def(nn("p1"), pvm(nn("b")));
+ dumpHistory(0, 30);
+ assertEquals(pvm(nn("b")), cem.retrievePrivlegeExpr(nn("p1")));
- def(nn("p1"), pvm(nn("b")));
- dumpHistory(0, 30);
- assertEquals(pvm(nn("b")), cem.retrievePrivlegeExpr(nn("p1")));
+ def(nn("p2"), pvm(nn("c")));
+ dumpHistory(0, 30);
+ assertEquals(pvm(nn("c")), cem.retrievePrivlegeExpr(nn("p2")));
- def(nn("p2"), pvm(nn("c")));
- dumpHistory(0, 30);
- assertEquals(pvm(nn("c")), cem.retrievePrivlegeExpr(nn("p2")));
-
- def(nn("p1"), pvm(nn("d")));
- dumpHistory(0, 30);
- assertEquals(pvm(nn("d")), cem.retrievePrivlegeExpr(nn("p1")));
+ def(nn("p1"), pvm(nn("d")));
+ dumpHistory(0, 30);
+ assertEquals(pvm(nn("d")), cem.retrievePrivlegeExpr(nn("p1")));
+ } finally {
+ mvm.stepout();
+ }
}
}
Modified: trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest2.java
==============================================================================
--- trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest2.java (original)
+++ trunk/procilege/src/test/java/procilege/test/pal/ComputationalEntityMgrTest2.java Mon Jun 11 07:09:56 2007
@@ -21,46 +21,51 @@
@Test
public void test1() {
- mvm.give(nm("testcase"));
+ mvm.give(nm("te"));
mvm.stepin();
+ try {
- def(nn("p1"), pvm(nn("a")));
- dumpHistory(0, 30);
- assertEquals(pvm(nn("a")), cem.retrievePrivlegeExpr(nn("p1")));
-
- PrivilegeForm pf1;
-
- pf1 = cem.retrievePrivlegeForm(nn("p1"));
- assertNotNull(pf1);
- int count = 0;
- Iterator<PrivilegeFormTerm> pftItr = pfa.normalTerms(pf1).iterator();
- while(pftItr.hasNext()) {
- PrivilegeFormTerm t = pftItr.next();
- if (nn("a").equals(t.getFunctionName())) {
- count++;
+ def(nn("p1"), pvm(nn("a")));
+ dumpHistory(0, 30);
+ assertEquals(pvm(nn("a")), cem.retrievePrivlegeExpr(nn("p1")));
+
+ PrivilegeForm pf1;
+
+ pf1 = cem.retrievePrivlegeForm(nn("p1"));
+ assertNotNull(pf1);
+ int count = 0;
+ Iterator<PrivilegeFormTerm> pftItr = pfa.normalTerms(pf1)
+ .iterator();
+ while (pftItr.hasNext()) {
+ PrivilegeFormTerm t = pftItr.next();
+ if (nn("a").equals(t.getFunctionName())) {
+ count++;
+ }
}
- }
- assertEquals(1, count);
+ assertEquals(1, count);
+
+ def(nn("p1"), pvc(nn("a"), nn("b")));
+ dumpHistory(0, 30);
+ assertEquals(pvc(nn("a"), nn("b")), cem
+ .retrievePrivlegeExpr(nn("p1")));
+
+ pf1 = cem.retrievePrivlegeForm(nn("p1"));
+ assertNotNull(pf1);
+ count = 0;
+ pftItr = pfa.normalTerms(pf1).iterator();
+ while (pftItr.hasNext()) {
+ PrivilegeFormTerm t = pftItr.next();
+ if (nn("a").equals(t.getFunctionName())) {
+ count++;
+ } else if (nn("b").equals(t.getFunctionName())) {
+ count++;
+ }
- def(nn("p1"), pvc(nn("a"), nn("b")));
- dumpHistory(0, 30);
- assertEquals(pvc(nn("a"), nn("b")), cem.retrievePrivlegeExpr(nn("p1")));
-
- pf1 = cem.retrievePrivlegeForm(nn("p1"));
- assertNotNull(pf1);
- count = 0;
- pftItr = pfa.normalTerms(pf1).iterator();
- while(pftItr.hasNext()) {
- PrivilegeFormTerm t = pftItr.next();
- if (nn("a").equals(t.getFunctionName())) {
- count++;
- } else if (nn("b").equals(t.getFunctionName())) {
- count++;
}
+ assertEquals(2, count);
+ } finally {
+ mvm.stepout();
}
- assertEquals(2, count);
-
- // cem.updatePrivlegeExpr(, nn("p1"));
}
}