Commit 0a2daab2 authored by Javier Baliosian's avatar Javier Baliosian
Browse files

Knowledge added.


Signed-off-by: Javier Baliosian's avatarbaliosian <javierba@fing.edu.uy>
parent f70e72ab
package uy.edu.fing.mina.fsa.logics;
import uy.edu.fing.mina.fsa.tf.TfI;
public class Implication {
TfI all;
TfI are;
public Implication(TfI all, TfI are) {
super();
this.all = all;
this.are = are;
}
}
\ No newline at end of file
package uy.edu.fing.mina.fsa.logics;
import java.util.Set;
public class Knowledge {
public static Set<Implication> implications;
public boolean verify(){
return true; //TODO to code verify implications
}
}
......@@ -10,8 +10,12 @@ import java.util.ArrayList;
import java.util.Arrays;
import java.util.Comparator;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import uy.edu.fing.mina.fsa.logics.quineMcCluskey.QmcFormula;
import uy.edu.fing.mina.fsa.logics.quineMcCluskey.Term;
......@@ -59,6 +63,8 @@ public class Utils {
TfI simplifiedTf = disjunctiveFormByMua(tf);
List<Term> termList = toTermList(simplifiedTf);
applyKnowledge(termList);
if (termList.size() > 0) {
// termList = expandDontCares(termList,0);
QmcFormula qmcf = new QmcFormula(termList);
......@@ -72,6 +78,42 @@ public class Utils {
}
// at this point I know that each term has all possible Tfs in the formula
private static void applyKnowledge(List<Term> termList) {
Set<Term> toremove = new HashSet<Term>();
Set<Implication> tosubstitute = new HashSet<Implication>();
// A -> -B, A and B are 1 in the term, then the term should be removed
// A -> B, A and B are both in the same term, then, B must be set as
// dontcare
// TODO A -> B, B is alone in a term, then, all occurrences of A in all the terms have to be
// substituted by B.
for (Implication impl : Knowledge.implications) {
for (Term term : termList) {
TfTerm a = null;
TfTerm b = null;
TfTerm notb = null;
for (TfTerm tft : term.varVals) {
if (impl.all.equals(tft.tf) && tft.b == 1) a = tft;
if (impl.are.equals(tft.tf) && tft.b == 1) b = tft;
if (impl.are.equals(tft.tf.not()) && tft.b == 1) notb = tft;
}
if (a != null && b != null) b.b = TfTerm.DontCare.b;
if (a != null && notb != null) toremove.add(term);
if (a == null && b != null) tosubstitute.add(impl);
}
}
termList.removeAll(toremove);
for (Term term : termList) {
for (Implication imp : tosubstitute) {
for (TfTerm tft : term.varVals) {
if (imp.all.equals(tft.tf) && tft.b == 1) tft.b = TfTerm.DontCare.b;
if (imp.are.equals(tft.tf)) tft.b = 1;
}
}
}
}
private static TfI termsListToTf(List<Term> termList) {
TfI out = null;
......@@ -200,9 +242,11 @@ public class Utils {
boolean skip = false;
for (int i = 0; i < term.varVals.length; i++) {
TfTerm tfterm = term.varVals[i];
if (tfMapTemp.get(tfterm.tf.getName()).b == TfTerm.DontCare.b) tfMapTemp.put(
tfterm.tf.getName(), tfterm);
else if (tfMapTemp.get(tfterm.tf.getName()).b != tfterm.b) skip = true;
if (tfMapTemp.get(tfterm.tf.getName()).b == TfTerm.DontCare.b)
tfMapTemp.put(tfterm.tf.getName(), tfterm);
else if (tfMapTemp.get(tfterm.tf.getName()).b != tfterm.b)
//term and its negation are both in the term list.
skip = true;
}
if (!skip) {
TfTerm[] tftermarray = tfMapTemp.values().toArray(new TfTerm[tfMapTemp.values().size()]);
......
......@@ -130,11 +130,13 @@ public class QmcFormula {
originalTermList = new ArrayList<Term>(termList);
int numVars = termList.get(0).getNumVars();
ArrayList<Term>[][] table = new ArrayList[numVars + 1][numVars + 1];
for (int dontKnows = 0; dontKnows <= numVars; dontKnows++) {
for (int ones = 0; ones <= numVars; ones++) {
table[dontKnows][ones] = new ArrayList<Term>();
}
}
for (int i = 0; i < termList.size(); i++) {
int dontCares = termList.get(i).countValues(TfTerm.DontCare.b);
int ones = termList.get(i).countValues((byte) 1);
......@@ -158,7 +160,6 @@ public class QmcFormula {
if (!termList.contains(combined)) {
termList.add(combined);
}
}
}
}
......
/*
* Created on 12-Aug-2004
*
* Copyright (C) 2004 Javier Baliosian
* All rights reserved.
* */
package uy.edu.fing.mina.fsa.test;
import uy.edu.fing.mina.fsa.logics.Utils;
import uy.edu.fing.mina.fsa.tf.SimpleTf;
/**
* @author Javier Baliosian &lt; <a
* href="mailto:jbaliosian@tsc.upc.es">jbaliosian@tsc.upc.es </a>&gt;
*/
public class SimplificationWithKnowledge {
/**
* uy.edu.fing.mina.omega.tffst.test 5, is the very example of the
* policy's paper. it works well but A <-> B and B <-> A must be unified
*
* @param args
*/
public static void main(String[] args) {
SimpleTf tfa = new SimpleTf();
tfa.setName("A");
SimpleTf tfb = new SimpleTf();
tfb.setName("B");
SimpleTf tfc = new SimpleTf();
tfc.setName("C");
SimpleTf tfd = new SimpleTf();
tfd.setName("D");
// System.out.println((
// tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd.not())))
// .or(tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc.not() .and(tfd))))
// .or(tfa .and(tfb .and(tfc .and(tfd))))
// ));
//
// System.out.println(Utils.simplify(
// tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd.not())))
// .or(tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc.not() .and(tfd))))
// .or(tfa .and(tfb .and(tfc .and(tfd))))
// ));
/*
*
{A0 B0 C0 }
{A0 B0 C1 }
{A0 B1 D1 }
{A1 B0 D0 }
{A1 B1 C0}
{A1 B1 C1 D1 }
*
*/
System.out.println(
tfa.not() .and(tfb.not() .and(tfc.not()))
.or(tfa.not() .and(tfb.not() .and(tfc)))
.or(tfa.not() .and(tfb .and(tfd)))
.or(tfa .and(tfb.not() .and(tfd.not())))
.or(tfa .and(tfb .and(tfc.not())))
.or(tfa .and(tfb .and(tfc.and(tfd))))
);
System.out.println((Utils.simplify(
tfa.not() .and(tfb.not() .and(tfc.not()))
.or(tfa.not() .and(tfb.not() .and(tfc)))
.or(tfa.not() .and(tfb .and(tfd)))
.or(tfa .and(tfb.not() .and(tfd.not())))
.or(tfa .and(tfb .and(tfc.not())))
.or(tfa .and(tfb .and(tfc.and(tfd))))
)));
// System.out.println((
// tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd.not())))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd.not()))))
// .or(tfa.not() .and(tfb .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd))))
// .or(tfa .and(tfb .and(tfc .and(tfd))))
// ));
//
// System.out.println(Utils.simplify(
// tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd.not())))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd.not()))))
// .or(tfa.not() .and(tfb .and(tfc.not() .and(tfd.not()))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd.not()))))
// .or(tfa .and(tfb .and(tfc .and(tfd.not()))))
// .or(tfa.not() .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc.not() .and(tfd))))
// .or(tfa.not() .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc .and(tfd))))
// .or(tfa .and(tfb .and(tfc .and(tfd))))
// ));
/*
000
010
011
110
101
111
*/
// System.out.println(Utils.simplify(
// tfa.not() .and(tfb.not() .and(tfc.not()))
// .or(tfa.not() .and(tfb .and(tfc.not())))
// .or(tfa.not() .and(tfb .and(tfc)))
// .or(tfa .and(tfb .and(tfc.not())))
// .or(tfa .and(tfb.not() .and(tfc)))
// .or(tfa .and(tfb .and(tfc)))
// ));
//
// System.out.println(Utils.simplify(
// tfa.or(tfb)
// .and(tfa.or(tfb.not()))
// ));
//
//
//-----
// System.out.println(
// (tfb .and(tfc .and(tfd)))
// .or(tfa .and(tfb.not() .and(tfc .and(tfd))))
// .or(tfa.not() .and(tfb .and(tfc.not() .and(tfd))))
// .or((tfb.not() .and(tfc.not() .and(tfd))))
// .or((tfb .and(tfc .and(tfd.not()))))
// .or((tfb .and(tfc.not() .and(tfd.not()))))
// .or((tfb.not() .and(tfc.not() .and(tfd.not()))))
// );
//
// TfTerm tfterma = new TfTerm(tfa, (byte) 1);
// TfTerm tftermb = new TfTerm(tfb, (byte) 1);
//
// TfTerm tftermna = new TfTerm((SimpleTf) tfa.not(), (byte) 0);
// TfTerm tftermnb = new TfTerm((SimpleTf) tfb.not(), (byte) 0);
// ( A and((!A or D ) and((!D or !A ) and (D and ( !D or A)))))
// System.out.println(tfa.and((tfa.not().or(tfb)).and((tfb.not().or(tfa.not()).and(tfb.and(tfb.not().or(tfa)))))));
//
// System.out.println(Utils.disjunctiveForm(tfa.and((tfa.not().or(tfb)).and((tfb.not().or(tfa.not()).and(tfb.and(tfb.not().or(tfa))))))));
//
// TfTerm[] termarray1 = new TfTerm[2];
// termarray1[0] = tfterma;
// termarray1[1] = tftermb;
//
// TfTerm[] termarray2 = new TfTerm[2];
// termarray2[0] = tfterma;
// termarray2[1] = tftermnb;
//
// Term term1 = new Term(termarray1);
// Term term2 = new Term(termarray2);
//
// List<Term> termList = new ArrayList<Term>();
// termList.add(term1);
// termList.add(term2);
//
// QmcFormula qmcf = new QmcFormula(termList);
// System.out.println(qmcf);
// qmcf.reduceToPrimeImplicants();
// System.out.println(qmcf);
// qmcf.reducePrimeImplicantsToSubset();
// System.out.println(qmcf);
//
}
}
\ No newline at end of file
......@@ -310,23 +310,21 @@ public int hashCode() {
/* (non-Javadoc)
* @see java.lang.Object#equals(java.lang.Object)
*/
@Override
public boolean equals(Object obj) {
if (this == obj) return true;
if (obj == null) return false;
if (!(obj instanceof Tf)) return false;
Tf other = (Tf) obj;
if (id != other.id) return false;
// if (identityTf == null) {
// if (other.identityTf != null) return false;
// } else if (!identityTf.equals(other.identityTf)) return false;
// if (identityType != other.identityType) return false;
if (not != other.not) return false;
// if (refersTo == null) {
// if (other.refersTo != null) return false;
// } else if (!refersTo.equals(other.refersTo)) return false;
return true;
}
@Override
public boolean equals(Object obj) {
if (this == obj)
return true;
if (obj == null)
return false;
if (!(obj instanceof Tf))
return false;
Tf other = (Tf) obj;
if (id != other.id)
return false;
if (not != other.not)
return false;
return true;
}
/**
* @return the weight
......
......@@ -408,7 +408,148 @@ public class Tffst implements Serializable {
//out.determinize();
return out;
}
/**
* COMPOSITION
* b o a (i.e. b(a(x)) )
*
* Constraint: a cannot have e-input labels and b cannot have e-output labels.
*
*
* \[
\begin{array}{ll}
\Pi=\{((p_1,p_2),d,r,(q_1,q_2),i)\mid
& p_1, d, \tau_1, q_1, i_1) \in \Pi_1, \\
& (p_2, \tau_2, r, q_2, i_2) \in \Pi_2, \\
& \tau_1 \wedge \tau_2 \\
& i=0 \: if\: i_1=0 \: or\: i_2=0\: or\: i_1 \neq i_2,\\
& i=1 \: if\: i_1=1\: and\: i_2=1, \\
& i=-1 \: if\: i_1=-1\: and\: i_2=-1\}\\
\multicolumn{2}{l}{\cup\;\{((p_1, p_2), \epsilon, d, (q_1, q_2), 0) \mid
(p_1,\epsilon,d',q_1,i_1)\in\Pi_1,(p_2,d',d,q_2,i_2)\in\Pi_2\}} \\
\multicolumn{2}{l}{\cup\;\{((p_{1},p_{2}),r,\epsilon,(q_{1},q_{2}),0)\mid
(p_1,r,d',q_1,i_1)\in\Pi_1,(p_2,d',\epsilon,q_2,i_2)\in\Pi_2\}}
\end{array}
\]
*
*
*
*
*/
static public Tffst composition(Tffst b, Tffst a) {
Tffst aSimple = a.toSingleLabelTransitions();
Tffst bSimple = b.toSingleLabelTransitions();
Tffst out = new Tffst();
Set<State> aStates = aSimple.getLiveStates();
Set<State> bStates = bSimple.getLiveStates();
HashMap<StatePair, State> newstates = new HashMap<StatePair, State>();
for (State aState : aStates){
for (State bState : bStates){
// get the new state that is equivalent to this pair, create it.
State outStartState = newstates.get(new StatePair(aState, bState));
if (outStartState == null) {
outStartState = new State();
newstates.put(new StatePair(aState, bState), outStartState);
if (aState.equals(aSimple.initial) && bState.equals(bSimple.initial))
out.initial = outStartState;
outStartState.setAccept(aState.isAccept() && bState.isAccept());
}
//add fake e/e transition loop
aState.addOutTran(new Transition(SimpleTf.Epsilon(),SimpleTf.Epsilon(),aState));
bState.addOutTran(new Transition(SimpleTf.Epsilon(),SimpleTf.Epsilon(),bState));
Set<Transition> aStateTrans = aState.getTransitions();
Set<Transition> bStateTrans = bState.getTransitions();
for (Transition at : aStateTrans) {
for (Transition bt : bStateTrans) {
TfI tOutLabelIn = null;
TfI tOutLabelOut = null;
try {
// epsilon as a especial tf
if (at.labelOut.isEpsilon() && bt.labelIn.isEpsilon()) {
tOutLabelIn = (TfI) at.labelIn.get(0).clone();
tOutLabelOut = (TfI) bt.labelOut.get(0).clone();
}
if (!at.labelOut.isEpsilon() && !bt.labelIn.isEpsilon()) {
// ct((p1,π1,π1,q1,1),(p2,π2,π2,q2,1))=((p1,p2),π1∧π2,π1∧π2,(q1,q2),1)
if (at.labelOut.get(0).getIdentityType() == 1 && bt.labelOut.get(0).getIdentityType() == 1) {
tOutLabelIn = ((TfI) at.labelOut.get(0).clone()).andSimple((TfI) bt.labelIn.get(0).clone());
tOutLabelOut = (TfI) tOutLabelIn.clone();
tOutLabelOut.setIdentityType(1);
tOutLabelOut.setRefersTo(tOutLabelIn);
}
// ct((p1,φ,π1,q1,0),(p2,π2,π2,q2,1))=((p1,p2),φ,π1∧π2,(q1,q2),0)
if (at.labelOut.get(0).getIdentityType() == 0 && bt.labelOut.get(0).getIdentityType() == 1) {
tOutLabelIn = (TfI) at.labelIn.get(0).clone();
tOutLabelOut = ((TfI) at.labelOut.get(0).clone()).andSimple((TfI) bt.labelIn.get(0).clone());
tOutLabelOut.setIdentityType(0);
}
// ct((p1,π1,π1,q1,1),(p2,π2,ψ,q2,0))=((p1,p2),π1∧π2,ψ,(q1,q2),0)
if (at.labelOut.get(0).getIdentityType() == 1 && bt.labelOut.get(0).getIdentityType() == 0) {
tOutLabelIn = ((TfI) at.labelOut.get(0).clone()).andSimple((TfI) bt.labelIn.get(0).clone());
tOutLabelOut = (TfI) bt.labelIn.get(0).clone();
tOutLabelOut.setIdentityType(0);
}
// ct((p1,φ,π1,q1,0),(p2,π2,ψ,q2,0))=((p1,p2),φ,ψ,(q1,q2),0) if
// satisfiable(π1∧π2)
if (at.labelOut.get(0).getIdentityType() == 1 && bt.labelOut.get(0).getIdentityType() == 0
&& ((TfI) at.labelOut.get(0).clone()).andSimple((TfI) bt.labelIn.get(0).clone()).satisfiable()) {
tOutLabelIn = (TfI) at.labelIn.get(0).clone();
tOutLabelOut = (TfI) bt.labelOut.get(0).clone();
tOutLabelOut.setIdentityType(0);
}
}
// {((p1,p2 ), ,ψ,(p1,q2),0)|p1 ∈ Q1,(p2,,ψ,q2,0) ∈ E2 }
; // TODO
// {((p1,p2 ),φ, ,(q1,p2),0)|p2 ∈ Q2,(p1,φ,,q1,0) ∈ E1 }
; // TODO
if (tOutLabelIn != null && tOutLabelOut != null) {
// get the new state that is equivalent to this pair, create it.
State outToState = newstates.get(new StatePair(at.getTo(), bt.getTo()));
if (outToState == null) {
outToState = new State();
newstates.put(new StatePair(at.getTo(), bt.getTo()), outToState);
if (at.getTo().equals(a.initial) && bt.getTo().equals(bSimple.initial))
out.initial = outToState;
outToState.setAccept(at.getTo().isAccept() && bt.getTo().isAccept());
}
outStartState.addOutTran(new Transition(tOutLabelIn, tOutLabelOut, outToState));
}
} catch (CloneNotSupportedException e) {
e.printStackTrace();
}
}
}
}
}
out.removeInputEpsilonLabel();
out.removeDeadTransitions();
//out.checkMinimizeAlways(); //TODO need this?
//out.setDeterministic(false);
//out.determinize();
return out;
}
/**
* Returns new Tffst that accepts the concatenation of the languages of this
* and the given Tffst.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment