Commit 74033978 authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Support unless construct (Closes #3)

parent 56aa1865
......@@ -149,9 +149,13 @@ public class Compile {
"sets #define as progress state label (prepend a '!' to define non-progress)", false);
parser.addOption(progress);
final BooleanOption dot = new BooleanOption('d',
"only write dot output (ltsmin/spins) \n");
parser.addOption(dot);
final BooleanOption dot = new BooleanOption('d',
"only write dot output (ltsmin/spins) \n");
parser.addOption(dot);
final BooleanOption java = new BooleanOption('J',
"Java escape semantics for unless statements (equivalent to SPIN's -J option) \n");
parser.addOption(java);
final BooleanOption no_cnf = new BooleanOption('C',
"Do not rewrite guards to CNF\n");
......@@ -273,7 +277,7 @@ public class Compile {
Options opts = new Options(verbose.isSet(), no_guards.isSet(),
must_write.isSet(), !no_cnf.isSet(),
nonever.isSet());
nonever.isSet(), java.isSet());
File outputDir = new File(System.getProperty("user.dir"));
if (dot.isSet()) {
......
......@@ -24,7 +24,6 @@ import java.util.Stack;
import spins.promela.compiler.Proctype;
import spins.util.StringWriter;
import spins.util.UnModifiableIterator;
/**
* An Automaton is a simple LTS that holds {@link State}s and {@link Transition}s. It can be used
......@@ -87,42 +86,79 @@ public class Automaton implements Iterable<State> {
return false;
}
private class Explorer implements Iterator<State> {
private Iterator<State> it;
private State init;
private State end;
public Explorer() {
this(startState, null);
}
public Explorer(State startState, State end) {
init = startState;
this.end = end;
init();
}
public boolean hasNext() { return it.hasNext(); }
public State next() { return it.next(); }
public void init() {
List<State> list = new ArrayList<State>();
Stack<State> stack = new Stack<State>();
Set<State> states = new HashSet<State>(Collections.singleton(startState));
stack.push(init);
while (!stack.isEmpty()) {
State next = stack.pop();
list.add(next);
for (final Transition out : next.output) {
State to = out.getTo();
if (to != end && to != null && states.add(to)) {
stack.push(to);
}
}
}
states = null;
stack = null;
it = list.listIterator();
}
public void remove() {
throw new UnsupportedOperationException();
}
};
/**
* Return a new Iterator that can be used to go over all States.
*
* @see java.lang.Iterable#iterator()
*/
public Iterator<State> iterator() {
return new UnModifiableIterator<State>() {
private Iterator<State> it;
public boolean hasNext() { return it.hasNext(); }
public State next() { return it.next(); }
public void init() {
List<State> list = new ArrayList<State>();
Stack<State> stack = new Stack<State>();
Set<State> states = new HashSet<State>(Collections.singleton(startState));
stack.push(startState);
while (!stack.isEmpty()) {
State next = stack.pop();
list.add(next);
for (final Transition out : next.output) {
if (out.getTo() != null && states.add(out.getTo())) {
stack.push(out.getTo());
}
}
}
states = null;
stack = null;
it = list.listIterator();
}
};
return new Explorer();
}
public void addUnless(final State start, final State end, State escape,
int priority) {
Iterable<State> main = new Iterable<State>() {
public Iterator<State> iterator() {
return new Explorer(start, end);
}
};
for (State s : main) {
for (Transition t : escape.output) {
Transition n = t.duplicateFrom(s);
n.setUnlessPriority(priority);
}
}
escape.delete();
}
/**
* @return The number of states that are reachable from the current starting state.
*/
......
......@@ -57,6 +57,8 @@ public class State {
private final Automaton automaton;
private int unlesses = 0;
private final List<Transition> out, in;
private List<String> labels;
......@@ -377,4 +379,8 @@ public class State {
public void addLabels(List<String> labels2) {
this.labels.addAll(labels2);
}
public int nextUnless() {
return unlesses++;
}
}
......@@ -49,6 +49,7 @@ public abstract class Transition implements ActionContainer {
private List<String> labels;
private int priority = -1;
protected Transition(final State from, final State to) {
if (from == null) {
......@@ -78,6 +79,7 @@ public abstract class Transition implements ActionContainer {
public Transition(Transition t, final State from, final State to) {
this(from, to);
if (t != null) {
this.priority = t.priority;
this.labels = t.labels;
}
}
......@@ -323,4 +325,13 @@ public abstract class Transition implements ActionContainer {
public List<String> getLabels() {
return labels;
}
public int getUnlessPriority() {
return priority ;
}
public void setUnlessPriority(int p) {
priority = p;
}
}
......@@ -96,9 +96,11 @@ public class LTSminDMWalker {
this.opts = opts;
}
}
private static Params sParams = new Params(null, null, new RWMatrix(null, null, null),
0, new Options(false, false, false, false, false));
private static RWMatrix DUMMY_MATRIX = new RWMatrix(null, null, null);
private static Options DUMMY_OPTIONS = new Options(false, false, false, false, false, false);
private static Params sParams = new Params(null, null, DUMMY_MATRIX,
0, DUMMY_OPTIONS);
public static void walkOneGuard(LTSminModel model, DepMatrix dm,
Expression e, int num) {
sParams.model = model;
......
......@@ -91,6 +91,7 @@ import spins.promela.compiler.ltsmin.matrix.LTSminGuardBase;
import spins.promela.compiler.ltsmin.matrix.LTSminGuardContainer;
import spins.promela.compiler.ltsmin.matrix.LTSminGuardNand;
import spins.promela.compiler.ltsmin.matrix.LTSminGuardOr;
import spins.promela.compiler.ltsmin.matrix.LTSminPCGuard;
import spins.promela.compiler.ltsmin.model.LTSminModel;
import spins.promela.compiler.ltsmin.model.LTSminState;
import spins.promela.compiler.ltsmin.model.LTSminTransition;
......@@ -123,6 +124,7 @@ import spins.promela.compiler.variable.VariableType;
public class LTSminTreeWalker {
private static final boolean SPLIT = false;
private static boolean UNLESS_JAVA_SEMANTICS = false;
public List<ReadAction> reads = new ArrayList<ReadAction>();
public List<SendAction> writes = new ArrayList<SendAction>();
......@@ -168,18 +170,21 @@ public class LTSminTreeWalker {
public static class Options {
public Options(boolean verbose, boolean no_gm, boolean must_write,
boolean cnf, boolean nonever) {
boolean cnf, boolean nonever,
boolean unless_java_semantics) {
this.verbose = verbose;
this.no_gm = no_gm;
this.must_write = must_write;
this.cnf = cnf;
this.nonever = nonever;
this.unless_java_semantics = unless_java_semantics;
}
public boolean nonever = false;
public boolean verbose = false;
public boolean no_gm = false;
public boolean must_write = false;
public boolean cnf = false;
public boolean unless_java_semantics = false;
}
TimeoutExpression timeout = null;
......@@ -192,6 +197,8 @@ public class LTSminTreeWalker {
Map<String, Expression> exports,
Expression progress) {
this.debug = new LTSminDebug(opts.verbose);
UNLESS_JAVA_SEMANTICS = opts.unless_java_semantics;
debug.say("Generating next-state function ...");
debug.say_indent++;
LTSminProgress report = new LTSminProgress(debug).startTimer();
......@@ -975,12 +982,16 @@ public class LTSminTreeWalker {
}
}}
for (LTSminTransition lt : begin.getOut()) {
createUnlessGuards (lt);
}
// update stack table
removeSearchStack (begin);
return begin;
}
/**
/**
* We use the DFS above to detect cycles containing only atomic states.
* The states on the stack are annotated with a number which only grows
* if atomicity changes from one stack state to the next (a transition
......@@ -1146,6 +1157,49 @@ public class LTSminTreeWalker {
return list;
}
/**
* Unless escape sequences are modeled in the state machine as follows.
*
* Consider the following Promela example:
* { a; b; c; } unless { g -> x; y; z }
*
* The generated LTS is:
*
* O---a--->O---b--->O---c--->X
* | / / ^
* |/------+-------/ /
* | /
* | z
* \--g:x-->O---y--->O---/
*
* (The unless transitions model each possible escape point)
*
* Nested escape sequences cause multiple outgoing unless transitions
* from a state. Their escape guards are prioritized according to the
* nesting semantics (see SpinS'/SPIN's '-J' command line option).
*
*/
private void createUnlessGuards(LTSminTransition lt) {
int prior1 = lt.getTransition().getUnlessPriority();
for (LTSminTransition other : lt.getBegin().getOut()) {
int prior2 = other.getTransition().getUnlessPriority();
if (lt == other || !prioritize(prior2, prior1)) continue;
LTSminGuardNand nand = new LTSminGuardNand();
for (LTSminGuardBase g : other.getGuards()) {
if (g instanceof LTSminPCGuard) continue;
nand.addGuard(g);
}
lt.addGuard(nand);
}
}
private boolean prioritize(int prior1, int prior2) {
if (prior1 == -1) return false;
if (prior2 == -1) return true; // prior1 != -1
return UNLESS_JAVA_SEMANTICS ? prior1 < prior2 : prior2 < prior1;
}
private Identifier getChannel(Action action) {
if (action instanceof ChannelSendAction) {
return ((ChannelSendAction)action).getIdentifier();
......
......@@ -46,6 +46,7 @@ public class Promela implements PromelaConstants {
private Proctype currentProc;
private Automaton automaton;
private int procNr = 0;
private int unlessPriority = 0;
private VariableType type;
private boolean declarations;
......@@ -676,6 +677,7 @@ public class Promela implements PromelaConstants {
Expression expr;
Token id, t;
State end = start;
State start1, end1;
Transition trans;
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case SEMICOLON:
......@@ -1041,6 +1043,18 @@ public class Promela implements PromelaConstants {
jj_consume_token(-1);
throw new ParseException();
}
}
if (jj_2_28(2147483647)) {
jj_consume_token(UNLESS);
start1 = new State(automaton, false);
end1 = sequence(start1, breakNode, false);
for (Transition tr : end1.input) {
tr.changeTo(end);
}
end1.delete();
automaton.addUnless(start, end, start1, unlessPriority++);
} else {
;
}
{if (true) return end;}
throw new Error("Missing return statement in function");
......
......@@ -66,6 +66,7 @@ public class Promela {
private Proctype currentProc;
private Automaton automaton;
private int procNr = 0;
private int unlessPriority = 0;
private VariableType type;
private boolean declarations;
......@@ -1087,6 +1088,7 @@ State sequence(State start, State breakNode, boolean inAtomic): {
Expression expr;
Token id, t;
State end = start;
State start1, end1;
Transition trans;
}{
( delim() (end=sequence(end, breakNode, inAtomic))?
......@@ -1199,7 +1201,21 @@ State sequence(State start, State breakNode, boolean inAtomic): {
(end=sequence(end, breakNode, inAtomic))?
| <LCURLY> end=sequence(start, breakNode, inAtomic) <RCURLY>
(end=sequence(end, breakNode, inAtomic))?
)) { return end; }
))
(
LOOKAHEAD(<UNLESS> sequence()) <UNLESS>
{
start1 = new State(automaton, false);
}
end1=sequence(start1, breakNode, false)
{
for (Transition tr : end1.input) {
tr.changeTo(end);
}
end1.delete();
automaton.addUnless(start, end, start1, unlessPriority++); }
)?
{ return end; }
}
void delim(): {}{
......
/*fullf12 is used to denote that no more enqueue operations can occur on fifo f12 in that cycle.
Its set to true if an enqueue occurred in a fifo even if there is space left in fifo.*/
#define __instances_reset 1
#define __instances_output1 1
#define __instances_output2 1
#define __instances_output3 1
#define __instances_output4 1
#define __instances_route12 1
#define __instances_route22 1
#define __instances_route32 1
#define __instances_route42 1
#define __instances_route11 1
#define __instances_route21 1
#define __instances_route31 1
#define __instances_route41 1
#define __instances_enqeuef11 1
#define __instances_enqeuef21 1
#define __instances_enqeuef31 1
#define __instances_enqeuef41 1
byte rule;
bool cycle, fullf12, fullf22, fullf32, fullf42, fullf13, fullf23, fullf33, fullf43;
int x, a, b, c, d, dst, dst1, dst2, dst3, dst4;
......
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