Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

\rho 4 transitions need not always violate system goal p_j, just has …

…to go back into the appropriate X-set
  • Loading branch information...
commit 47c2734967ce31c0393ddcd4631d473af47bbc76 1 parent 82f3f2c
Vasumathi Raman authored cfinucane committed
Showing with 8 additions and 7 deletions.
  1. +8 −7 src/etc/jtlv/GROne/GROneGame.java
View
15 src/etc/jtlv/GROne/GROneGame.java
@@ -1140,23 +1140,23 @@ public boolean calculate_counterstrategy(BDD ini, boolean enable_234, boolean de
if (rank_i != -1 && rank_j != -1) {
if (p_az == 0) {
if (p_c == 0) {
- input = input.or(((p_st.and((primed_cur_succ.and((controlStates(env,sys,sys.justiceAt(p_j).not().and(Env.unprime(primed_cur_succ).and(env.justiceAt(rank_i)).and(x2_mem[p_j][rank_i][p_az][p_c]))))))))
+ input = input.or(((p_st.and((primed_cur_succ.and((controlStates(env,sys,(Env.unprime(primed_cur_succ).and(env.justiceAt(rank_i)).and(x2_mem[p_j][rank_i][p_az][p_c]))))))))
//this next clause is probably superfluous because of \rho_1
.and((controlStates(env,sys,Env.FALSE())).not())));
} else {
- input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,sys.justiceAt(p_j).not().and(Env.unprime(primed_cur_succ).and(x2_mem[p_j][rank_i][p_az][p_c-1])))))))
+ input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,(Env.unprime(primed_cur_succ).and(x2_mem[p_j][rank_i][p_az][p_c-1])))))))
.and((controlStates(env,sys,Env.FALSE())).not())));
}
} else {
if (p_c == 0) {
- input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,sys.justiceAt(p_j).not().and(Env.unprime(primed_cur_succ).and(env.justiceAt(rank_i)).and(x2_mem[p_j][rank_i][p_az][p_c])))))))
+ input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,(Env.unprime(primed_cur_succ).and(env.justiceAt(rank_i)).and(x2_mem[p_j][rank_i][p_az][p_c])))))))
.and((controlStates(env,sys,z2_mem[p_az-1])).not())));
} else {
- input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,sys.justiceAt(p_j).not().and(Env.unprime(primed_cur_succ).and(x2_mem[p_j][rank_i][p_az][p_c-1])))))))
+ input = input.or(((p_st.and(primed_cur_succ.and((controlStates(env,sys,(Env.unprime(primed_cur_succ).and(x2_mem[p_j][rank_i][p_az][p_c-1])))))))
.and((controlStates(env,sys,z2_mem[p_az-1])).not())));
}
@@ -1173,7 +1173,7 @@ public boolean calculate_counterstrategy(BDD ini, boolean enable_234, boolean de
}
- assert (!(input.isZero() && det)) : p_st+"No successor was found";
+ assert (!(input.isZero() && det)) : p_st + "No successor was found";
addState(new_state, input, new_i, new_j, aut, st_stack, i_stack, j_stack, det);
@@ -1259,12 +1259,13 @@ private void addState(RawCState new_state, BDD input, int new_i, int new_j, Stac
//Make sure this is a safe successor state
if (!sys_succ.and(sys.trans()).isZero()) {
- //System.out.println("Adding system successor = " + sys_succ + " of " + new_state.get_state());
-
+
RawCState gsucc = new RawCState(aut.size(), sys_succ, new_j, new_i, inputOne);
idx = aut.indexOf(gsucc); // the equals doesn't consider
// the id number.
if (idx == -1) {
+ //System.out.println("Adding system successor = " + sys_succ + " of " + new_state.get_state());
+
st_stack.push(sys_succ);
i_stack.push(new_i);
j_stack.push(new_j);
Please sign in to comment.
Something went wrong with that request. Please try again.