Commit 9d3ca1a2 authored by fthoma's avatar fthoma
Browse files

all operator and some small changes

parent 1f66dc33
/** Bounded number of muddy children
**/
property: {exists i: m_i /\ atMost(m,4) !} // Replace 4 by your preferred value
property: {exists i: m_i /\ atMost(m,2) !} // Replace 4 by your preferred value
show(true) /\ // show model
debug(model) /\
{forall i: <i>!m_i !}*
show(true) /\
debug(relation) /\ //show relation
false //iteration has to stop: someone will eventually know
false /\ //iteration has to stop: someone will eventually know
debug(model)
;
/** Model declaration **/
......@@ -21,7 +24,7 @@ q0 on clean,false,clean to q0;
q0 on clean,true,muddy to q1;
q0 on muddy,true,clean to q1;
q0 on muddy,true,muddy to q1;
q0 on clean,true,muddy to q1;
q0 on clean,true,clean to q1;
q1 on muddy,false,muddy to q1;
q1 on clean,false,clean to q1;
/** Everyone is blind. But the announcement makes everyone aware of agent 0's
status.
**/
property:
{ !exists i, i=2 !} // at most 3 agents
property:
//{ !exists i, i=3 !} // at most 2 agents
debug(model) /\
{ exists i, i=0 /\ m_i !!}
{ exists i, i=0 /\ m_i !!}
{ exists i, i=0 /\ m_i !!}
debug(model)
//{ exists i, i=0 /\ m_i !!}
{ exists j: m_j /\ <j> !m_j !}*
debug(model) /\
debug(relation) /\
false
;
/** Model declaration (same as for the bounded case) **/
......@@ -18,8 +19,6 @@ location clean: {};
init: q0;
accepting: q1;
q0 on clean,false,muddy to q0;
q0 on muddy,false,clean to q0;
q0 on muddy,false,muddy to q0;
q0 on clean,false,clean to q0;
......@@ -28,7 +27,5 @@ q0 on muddy,true,clean to q1;
q0 on muddy,true,muddy to q1;
q0 on clean,true,clean to q1;
q1 on clean,false,muddy to q1;
q1 on muddy,false,clean to q1;
q1 on muddy,false,muddy to q1;
q1 on clean,false,clean to q1;
......@@ -3,15 +3,17 @@
property:
// Enforce c^*m^*
{forall i: (exists j: j=i+1 /\ !m_j) -> !m_i !}
show(true) /\
// show(true) /\
// Father: there exists a muddy child
{exists i: m_i !}
//debug(model) /\
// debug(model) /\
//Iterated announcement: there is still a mudheaded child who doesn't know it
{exists j: m_j /\ <j> !m_j !}*
//will show you the disappearance relation automaton:
//s<=t iff there are more muddy children in t, ie L_{<=} = (c,c)*(c,m)*(m,m)*
debug(relation) /\ false
debug(relation) /\
debug(model) /\
false
;
/** Model declaration (same as for the bounded case) **/
......@@ -28,7 +30,7 @@ q0 on clean,false,clean to q0;
q0 on clean,true,muddy to q1;
q0 on muddy,true,clean to q1;
q0 on muddy,true,muddy to q1;
q0 on clean,true,muddy to q1;
q0 on clean,true,clean to q1;
q1 on muddy,false,muddy to q1;
q1 on clean,false,clean to q1;
/** Bounded number of dining cryptographers
**/
property:
{ !exists i, i=3 !} // at most 3 agents
show(true) /\
debug(model) //show relation
;
/** Model declaration **/
AP: {p,c};
location pc: {p,c};
location p: {p};
location c: {c};
location x: {};
init: q0;
accepting: q1;
q0 on p,false,p to q0;
q0 on p,false,pc to q0;
q0 on p,false,c to q0;
q0 on p,false,x to q0;
q0 on pc,false,p to q0;
q0 on pc,false,pc to q0;
q0 on pc,false,c to q0;
q0 on pc,false,x to q0;
q0 on c,false,p to q0;
q0 on c,false,pc to q0;
q0 on c,false,c to q0;
q0 on c,false,x to q0;
q0 on x,false,p to q0;
q0 on x,false,pc to q0;
q0 on x,false,c to q0;
q0 on x,false,x to q0;
q0 on p,true,p to q1;
q0 on pc,true,pc to q1;
q0 on c,true,c to q1;
q0 on x,true,x to q1;
q1 on p,false,p to q1;
q1 on p,false,pc to q1;
q1 on p,false,c to q1;
q1 on p,false,x to q1;
q1 on pc,false,p to q1;
q1 on pc,false,pc to q1;
q1 on pc,false,c to q1;
q1 on pc,false,x to q1;
q1 on c,false,p to q1;
q1 on c,false,pc to q1;
q1 on c,false,c to q1;
q1 on c,false,x to q1;
q1 on x,false,p to q1;
q1 on x,false,pc to q1;
q1 on x,false,c to q1;
q1 on x,false,x to q1;
property:
show(true) /\
// debug(model) /\
//{ exists i, i=0 /\ !p_i \/ !c_i !!} //whether pi and not ci with i=0
//{ exists i, i=0 /\ ((!c_i \/ !p_i) \/ (c_i /\ !p_i)) !!} //whether pi xor ci with i=0
//(!((!ci and pi) or (ci and !pi)) and ci+1) or (((!ci and pi) or (ci and !pi)) and !ci+1) //ci xor pi xor ci+1
{ exists i, i=0 /\ ((((!c_i \/ !p_i) \/ (c_i /\ !p_i)) /\ !(exists j: j=i+1 /\ c_j)) \/ ((!(!c_i \/ !p_i) \/ (c_i /\ !p_i)) /\ (exists j: j=i+1 /\ c_j))) !!} //whether pi xor ci xor ci+1 with i=0
//phi_i = alle a knowwhether A_j (j<i) und nicht knowwhether A_i
debug(model)
;
/** Model declaration **/
AP: {p,c};
location pc: {p,c};
location p: {p};
location c: {c};
location x: {};
init: q0;
accepting: q1;
q0 on p,false,p to q0;
q0 on p,false,pc to q0;
q0 on p,false,c to q0;
q0 on p,false,x to q0;
q0 on pc,false,p to q0;
q0 on pc,false,pc to q0;
q0 on pc,false,c to q0;
q0 on pc,false,x to q0;
q0 on c,false,p to q0;
q0 on c,false,pc to q0;
q0 on c,false,c to q0;
q0 on c,false,x to q0;
q0 on x,false,p to q0;
q0 on x,false,pc to q0;
q0 on x,false,c to q0;
q0 on x,false,x to q0;
q0 on p,true,p to q1;
q0 on pc,true,pc to q1;
q0 on c,true,c to q1;
q0 on x,true,x to q1;
q1 on p,false,p to q1;
q1 on p,false,pc to q1;
q1 on p,false,c to q1;
q1 on p,false,x to q1;
q1 on pc,false,p to q1;
q1 on pc,false,pc to q1;
q1 on pc,false,c to q1;
q1 on pc,false,x to q1;
q1 on c,false,p to q1;
q1 on c,false,pc to q1;
q1 on c,false,c to q1;
q1 on c,false,x to q1;
q1 on x,false,p to q1;
q1 on x,false,pc to q1;
q1 on x,false,c to q1;
q1 on x,false,x to q1;
[∃i:(( (((¬ci/\pi)\/(ci/\¬pi))/\¬(∃j:((j=i+1)/\cj))) \/ ¬(((¬ci/\pi)\/(ci/\¬pi))/\∃j:((j=i+1)/\cj)) ));!!]
[¬((¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ¬(∃j:((j = i + 1) /\ (c at j ?));))) /\ ¬(( ((¬ci/\pi)\/(ci/\¬pi)) /\ ∃j:((j=i+1)/\cj) )))));!!]
Property: (show(T) /\ [∃i:((i = 0) /\ ¬((¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ¬(∃j:((j = i + 1) /\ (c at j ?));))) /\ ¬(¬((¬((¬(¬(¬((¬((ci)) /\ ¬(¬((p at i ?) /\ ¬(((ci) /\ ¬((pi) ;)
Property: (show(T) /\ [∃i:((i = 0) /\ ¬((¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ¬(∃j:((j = i + 1) /\ (c at j ?));))) /\ ¬((¬((¬(¬(¬((¬((ci)) /\ ¬(¬((p at i ?) /\ ¬(((ci) /\ ¬((pi) ;
Property: (show(T) /\ [∃i:((i = 0) /\ ¬((¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ¬(∃j:((j = i + 1) /\ (c at j ?));))) /\ ¬((¬(¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?))))))) /\ ∃j:((j = i + 1) /\ (c at j ?));)))));!!]debug(model))
Property: (show(T) /\ [∃i:((i = 0) /\ ¬((¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ¬(∃j:((j = i + 1) /\ (c at j ?));))) /\ ¬(¬((¬((¬(¬(¬((¬((c at i ?)) /\ ¬(¬((p at i ?))))))) /\ ¬(((c at i ?) /\ ¬((p at i ?)))))) /\ ∃j:((j = i + 1) /\ (c at j ?));))))));!!]debug(model))
\ No newline at end of file
/** Bounded number of muddy children
**/
property: show(true) /\
{exists i: m_i /\ atMost(m,2) !} // Replace 4 by your preferred value
show(true) /\ // show model
{forall i: <i>!m_i !}*
debug(relation) /\ //show relation
false //iteration has to stop: someone will eventually know
;
/** Model declaration **/
AP: {m};
location muddy: {m};
location clean: {};
init: q0;
accepting: q1;
q0 on muddy,false,clean to q0;
q0 on clean,false,muddy to q0;
q0 on clean,true,clean to q1;
q0 on muddy,true,muddy to q1;
q1 on clean,false,muddy to q1;
q1 on muddy,false,clean to q1;
......@@ -67,7 +67,7 @@ modalQuantification
| '{' ppal '!}' ppal #pa
| '{' ppal '!}*' ppal #pastar
| '{' ppal '!!}' ppal #paw
// TODO pawstar
| '{' ppal '!!}*' ppal #pawstar
;
indexVar: ID;
......
package arg.pepsistemic.ppal;
import java.util.ArrayList;
import java.util.HashSet;
import arg.pepsistemic.common.Morphism;
import arg.pepsistemic.common.Multiplier;
import arg.pepsistemic.learning.Learner;
import arg.pepsistemic.ppal.ValuationAlphabet.ValVector;
import net.automatalib.automata.fsa.DFA;
import net.automatalib.automata.fsa.NFA;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.automata.fsa.impl.compact.CompactNFA;
import net.automatalib.commons.util.Pair;
import net.automatalib.commons.util.Triple;
import net.automatalib.util.automata.fsa.NFAs;
import net.automatalib.words.Alphabet;
import net.automatalib.words.impl.Alphabets;
/**
* Operator of the form {φ!!}*ψ ie, does there exists k such that {φ!!}^k ψ holds
*
* @param <T>
*/
public class PAWstar<T extends State> extends Formula<T> {
protected Formula<T> extAssumption;
protected Formula<T> assumption;
protected Formula<T> conclusion;
Formula<T> top;
Formula.Restricter<T> projector;
public PAWstar(Formula<T> assumption, Formula<T> conclusion) {
super();
this.assumption = assumption;
this.extAssumption = assumption.copy();
this.conclusion = conclusion;
top = new Top<T>();
}
@Override
public String toString() {
return "[" + assumption + "!!]*" + conclusion;
}
public PAWstarLearner getLearner(CompactNFA<Pair<Triple<T, Boolean, T>, ValVector>> ext) {
CompactDFA<Pair<Triple<T, Boolean, T>, ValVector>> model = NFAs.determinize(ext);
CompactNFA<T> stateSpace = projector.build(top.semantics(ext));
CompactNFA<Pair<T,T>> stateSpace2 = (new Multiplier.SynchronousProduct<T,T>(alpha2)).build(stateSpace, stateSpace, alpha, alpha);
PAWstarLearner learner = new PAWstarLearner(alpha, alpha2, NFAs.determinize(stateSpace), NFAs.determinize(stateSpace2), model);
return learner;
}
@Override
protected CompactNFA<Pair<T, ValVector>> semantics(CompactNFA<Pair<Triple<T, Boolean, T>, ValVector>> model) {
PAWstarLearner learner = getLearner(model);
//1° learn the disappearance relation R, using the learner below
DFA<?, Pair<T,T>> disappearR = learner.learn();
System.out.println("relation size: " + disappearR.size());
conclusion.notifyRelation(disappearR, alpha2);
//2° Compute S_fin = complement of max(R)
CompactNFA<T> sfin = (new NonMaximizer(alpha)).build(disappearR, alpha2);
//3° Compute {s| exists t: s\in [[ψ]](tR.) } ie the operatorExt(R) for the conclusion part, then restricted on 1st coordinate
// 3.1°/ compute extended model.
CompactNFA<Pair<Triple<T, Boolean, T>, ValVector>> extModel;
extModel = c1.build(model, disappearR, modelAlpha, alpha2);
extModel = c2.build(extModel, disappearR, extModelAlpha, alpha2);
extModel = Helper.minimize(extModel);
// 3.2°/ compute semantics for conclusion (! on extended alphabet !)
NFA<Integer,Pair<T, ValVector>> extSem = conclusion.semantics(extModel);
//4° return union of 2 and 3
return (new FinalJoin()).build(sfin, extSem, alpha, extSemAlpha);
//throw new RuntimeException("Not implemented");
}
class FinalJoin extends Multiplier<Pair<T, ValVector>, T, Pair<T, ValVector>> {
public FinalJoin() {
super(semAlpha);
}
@Override
public <S1,S2> CompactNFA<Pair<T,ValVector>> build(NFA<S1,T> auto1, NFA<S2,Pair<T,ValVector>> auto2, Alphabet<T> alpha1, Alphabet<Pair<T,ValVector>> alpha2) {
// we want complete automata (hence partial = false)
return super.build(
NFAs.determinize(auto1, alpha1, false, true),
NFAs.determinize(auto2, alpha2, false, true),
alpha1,
alpha2
);
}
// It's an OR
@Override
protected <S1, S2> boolean isAcceptingPair(NFA<S1,T> auto1, NFA<S2,Pair<T,ValVector>> auto2, S1 s1, S2 s2) {
return auto1.isAccepting(s1) || auto2.isAccepting(s2);
}
@Override
protected Pair<T, ValVector> combineInputs(T x1, Pair<T, ValVector> x2) {
if(!x1.equals(x2.getFirst()))
return null;
ValVector v = x2.getSecond().project(valAlpha);
assert(v.x == 0); // In any case, valAlpha should have no variable (in this implementation)
return Pair.of(x1, v);
}
}
/**
* class to compute S_fin from a disappearance relation
*
*/
class NonMaximizer extends Multiplier<T,Pair<T,T>,Pair<T,T>> {
public NonMaximizer(Alphabet<T> alpha) {
super(alpha);
}
@Override
protected <S1, S2> boolean isAcceptingPair(NFA<S1,Pair<T,T>> auto1, NFA<S2,Pair<T,T>> auto2, S1 s1, S2 s2) {
return !auto1.isAccepting(s1) || auto2.isAccepting(s2);
}
public <S1,S2> CompactNFA<T> build(NFA<S1,Pair<T,T>> auto, Alphabet<Pair<T,T>> alpha) {
// partial = false ! We want a complete automaton...
CompactDFA<Pair<T,T>> det = NFAs.determinize(auto, alpha, false, true);
return super.build(det, det, alpha, alpha);
}
@Override
protected T combineInputs(Pair<T, T> x1, Pair<T, T> x2) {
if(!x1.getFirst().equals(x2.getSecond()) || !x1.getSecond().equals(x2.getFirst()))
return null;
return x1.getSecond();
}
}
Alphabet<T> alpha;
Alphabet<Pair<T,T>> alpha2;
Alphabet<Pair<Triple<T,Boolean,T>,ValVector>> modelAlpha;
Alphabet<Pair<T,ValVector>> semAlpha;
ValuationAlphabet valAlpha;
Alphabet<Pair<Triple<T,Boolean,T>,ValVector>> extModelAlpha;
Alphabet<Pair<T,ValVector>> extSemAlpha;
ValuationAlphabet extValAlpha;
@Override
protected void setAlphabets(Alphabet<Pair<Triple<T, Boolean, T>, ValVector>> model,
Alphabet<Pair<T, ValVector>> sem, ValuationAlphabet valAlpha) {
assert(valAlpha.size() == 1); // Cannot deal with free variables
this.modelAlpha = model;
this.semAlpha = sem;
this.valAlpha = valAlpha;
// We build the list of states to reason on, now
HashSet<T> states = new HashSet<T>();
HashSet<Triple<T,Boolean,T>> trans = new HashSet<Triple<T,Boolean,T>>();
for(Pair<Triple<T, Boolean, T>, ValVector> symb: model) {
states.add(symb.getFirst().getFirst());
trans.add(symb.getFirst());
}
alpha = Alphabets.fromCollection(states);
alpha2 = Multiplier.SynchronousProduct.buildAlphabet(alpha,alpha);
extValAlpha = valAlpha.extendConditionalState(new ArrayList<State>(states));
extSemAlpha = Multiplier.SynchronousProduct.buildAlphabet(alpha, extValAlpha);
extModelAlpha = Multiplier.SynchronousProduct.buildAlphabet(new ArrayList<Triple<T,Boolean,T>>(trans), extValAlpha);
assumption.setAlphabets(model, sem, valAlpha);
conclusion.setAlphabets(extModelAlpha, extSemAlpha, extValAlpha);
extAssumption.setAlphabets(extModelAlpha, extSemAlpha, extValAlpha);
top.setAlphabets(model, sem, valAlpha);
projector = new Formula.Restricter<T>(alpha);
// For the learner
c1 = new ConditionExtender(extModelAlpha, extValAlpha, true);
c2 = new ConditionExtender(extModelAlpha, extValAlpha, false);
r1 = new Restricter(modelAlpha, true);
r2 = new Restricter(modelAlpha, false);
uncond = new Unconditionner(alpha2);
}
ConditionExtender c1, c2;
Restricter r1, r2;
Unconditionner uncond;
class PAWstarLearner extends Learner<T> {
public PAWstarLearner(Alphabet<T> alpha, Alphabet<Pair<T, T>> alpha2, CompactDFA<T> stateSpace,
CompactDFA<Pair<T, T>> stateSpace2, CompactDFA<Pair<Triple<T, Boolean, T>, ValVector>> model) {
super(alpha, alpha2, stateSpace, stateSpace2);
this.model = model;
}
CompactDFA<Pair<Triple<T, Boolean, T>, ValVector>> model;
/**
* Compute Semantics restricted semantics of assumption
*/
@Override
protected CompactDFA<T> operator(CompactDFA<T> input) {
//1°/ compute model restricted to input
assert(model != null);
CompactNFA<Pair<Triple<T,Boolean,T>,ValVector>> extModel = r1.build(model, input, modelAlpha, alpha);
extModel = r2.build(extModel, input, modelAlpha, alpha);
extModel = Helper.minimize(extModel); //TODO huge improvement (maybe useless later)
//2°/ compute assumption.semantics of restricted model
CompactNFA<Pair<T,ValVector>> sem = assumption.semantics(extModel);
return NFAs.determinize(projector.build(sem));
}
/**
* Compute F(.R) = {(s,t) | t in F({u | (s,u) in R})}
*/
@Override
protected CompactDFA<Pair<T, T>> operatorExt(CompactDFA<Pair<T, T>> input) {
// 1°/ compute extended model. Where ValVector is conditionally related to input
// as for the PA semantics, we have to restrict both source and destination
CompactNFA<Pair<Triple<T, Boolean, T>, ValVector>> extModel;
extModel = c1.build(model, input, modelAlpha, alpha2);
extModel = c2.build(extModel, input, extModelAlpha, alpha2);
extModel = Helper.minimize(extModel);
// 2°/ compute semantics of assumption (! on extended valAlphabet !)
CompactNFA<Pair<T, ValVector>> sem = extAssumption.semantics(extModel);
// 3°/ convert back to a CompactDFA<Pair<T,T>>
return NFAs.determinize(uncond.build(sem), true, true);
}
}
/**
* Restriction of the state space of a model
*
*/
class Restricter extends Multiplier<Pair<Triple<T,Boolean,T>,ValVector>, Pair<Triple<T,Boolean,T>,ValVector>, T> {
boolean source;
public Restricter(Alphabet<Pair<Triple<T, Boolean, T>, ValVector>> alpha, boolean source) {
super(alpha);
this.source = source;
}
@Override
protected Pair<Triple<T, Boolean, T>, ValVector> combineInputs(Pair<Triple<T, Boolean, T>, ValVector> x1,
T x2) {
if((source && !x1.getFirst().getFirst().equals(x2)) || (!source && !x1.getFirst().getThird().equals(x2)))
return null;
return x1;
}
}
/**
* Add state condition
*
*/
class ConditionExtender extends Multiplier<Pair<Triple<T, Boolean, T>, ValVector>, Pair<Triple<T, Boolean, T>, ValVector>, Pair<T,T>> {
boolean source = true;
ValuationAlphabet valAlpha;
public ConditionExtender(Alphabet<Pair<Triple<T, Boolean, T>, ValVector>> alpha, ValuationAlphabet valAlpha, boolean source) {
super(alpha);
this.source = source;
this.valAlpha = valAlpha;
}
@Override
protected Pair<Triple<T, Boolean, T>, ValVector> combineInputs(Pair<Triple<T, Boolean, T>, ValVector> x1,
Pair<T, T> x2) {
//the one to put as a condition
State cond = (State) x2.getFirst();
State st1 = (State) x2.getSecond();
State st2 = source?x1.getFirst().getFirst(): x1.getFirst().getThird();
assert(st1 != null);
if(!st2.equals(st1))
return null;
ValVector newVal = valAlpha.combine(x1.getSecond(), cond);
if(newVal == null)
return null;
return Pair.of(x1.getFirst(), newVal);
}
}
/**
* Goes from a state condition back to a relation
* NB: it's a bijective translation so maybe a simple alphabet swap could do …
*/
class Unconditionner extends Morphism<Pair<T,ValVector>,Pair<T,T>> {
public Unconditionner(Alphabet<Pair<T, T>> alpha2) {
super(alpha2);
}
@Override
public Pair<T, T> convert(Pair<T, ValVector> symbol) {
@SuppressWarnings("unchecked")
T cond = (T) symbol.getSecond().getStateCond();
assert(cond!= null);
return Pair.of(cond, symbol.getFirst());
}
}