Commit 56aa1865 authored by Alfons Laarman's avatar Alfons Laarman

Small refactor

parent 759a8c73
......@@ -35,8 +35,12 @@ public class ActionTransition extends Transition {
* @param from
* @param to
*/
public ActionTransition(Transition t, final State from, final State to) {
super(t, from, to);
sequence = new Sequence();
}
public ActionTransition(final State from, final State to) {
super(from, to);
super(null, from, to);
sequence = new Sequence();
}
......@@ -53,7 +57,7 @@ public class ActionTransition extends Transition {
*/
@Override
public Transition duplicateFrom(State from) {
final ActionTransition t = new ActionTransition(from, getTo());
final ActionTransition t = new ActionTransition(this, from, getTo());
t.sequence.add(sequence);
return t;
}
......
......@@ -25,8 +25,12 @@ public class ElseTransition extends Transition {
* @param to
* The destination state.
*/
public ElseTransition(Transition t, final State from, final State to) {
super(t, from, to);
}
public ElseTransition(final State from, final State to) {
super(from, to);
super(null, from, to);
}
/**
......@@ -34,7 +38,7 @@ public class ElseTransition extends Transition {
*/
@Override
public Transition duplicateFrom(State from) {
final Transition t = new ElseTransition(from, getTo());
final Transition t = new ElseTransition(this, from, getTo());
return t;
}
......
......@@ -28,16 +28,20 @@ public class EndTransition extends Transition {
* @param from
* The starting state.
*/
public EndTransition(Transition t, final State from) {
super(t, from, null);
}
public EndTransition(final State from) {
super(from, null);
}
/**
* @see spins.promela.compiler.automaton.Transition#duplicateFrom(State)
*/
@Override
public Transition duplicateFrom(State from) {
final Transition t = new EndTransition(from);
final Transition t = new EndTransition(this, from);
return t;
}
......
......@@ -34,6 +34,10 @@ public class GotoTransition extends Transition {
* @param text
* The label to where this transition should jump to.
*/
public GotoTransition(Transition t, final State from, final State to, final String text) {
super(t, from, to);
this.text = text;
}
public GotoTransition(final State from, final State to, final String text) {
super(from, to);
this.text = text;
......@@ -44,7 +48,7 @@ public class GotoTransition extends Transition {
*/
@Override
public Transition duplicateFrom(State from) {
final Transition t = new GotoTransition(from, getTo(), text);
final Transition t = new GotoTransition(this, from, getTo(), text);
return t;
}
......
// Copyright 2010, University of Twente, Formal Methods and Tools group
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
package spins.promela.compiler.automaton;
/**
* Represents an ending transition of a neverclaim, that generates to code the end the current
* neverclaim in Promela.
*
* @author Marc de Jonge
*/
public class NeverEndTransition extends EndTransition {
/**
* Constructor of NeverEndTransition using only the from state. The state where it ends is not
* relevant.
*
* @param from
* The starting state.
*/
public NeverEndTransition(final State from) {
super(from);
}
/**
* @see spins.promela.compiler.automaton.EndTransition#duplicateFrom(State)
*/
@Override
public Transition duplicateFrom(State from) {
final Transition t = new NeverEndTransition(from);
return t;
}
}
......@@ -174,7 +174,6 @@ public class State {
public boolean isEndingState() {
for (Transition trans : out) {
if (trans instanceof EndTransition ||
trans instanceof NeverEndTransition ||
null == trans.getTo())
return true;
}
......
......@@ -49,16 +49,8 @@ public abstract class Transition implements ActionContainer {
private List<String> labels;
/**
* Constructor of Transition. Creates a {@link Transition} from one {@link State} to an other.
* Both the from and to state must be part of the same automaton.
*
* @param from
* The {@link State} where the {@link Transition} must start.
* @param to
* The {@link State} where the {@link Transition} must end.
*/
public Transition(final State from, final State to) {
protected Transition(final State from, final State to) {
if (from == null) {
throw new IllegalArgumentException("A transition must always come from somewhere!");
}
......@@ -74,6 +66,22 @@ public abstract class Transition implements ActionContainer {
transId = TransitionIdCounter.nextId();
}
/**
* Constructor of Transition. Creates a {@link Transition} from one {@link State} to an other.
* Both the from and to state must be part of the same automaton.
*
* @param from
* The {@link State} where the {@link Transition} must start.
* @param to
* The {@link State} where the {@link Transition} must end.
*/
public Transition(Transition t, final State from, final State to) {
this(from, to);
if (t != null) {
this.labels = t.labels;
}
}
/**
* Adds a new action to this Transition. The default implementation always throws an
* {@link IllegalArgumentException}, because by default these can not be added (some subclasses
......
......@@ -31,6 +31,10 @@ public class UselessTransition extends Transition {
* @param text
* The text for this useless transition
*/
public UselessTransition(Transition t, final State from, final State to, final String text) {
super(t, from, to);
this.text = text;
}
public UselessTransition(final State from, final State to, final String text) {
super(from, to);
this.text = text;
......@@ -41,7 +45,7 @@ public class UselessTransition extends Transition {
*/
@Override
public Transition duplicateFrom(State from) {
final Transition t = new UselessTransition(from, getTo(), text);
final Transition t = new UselessTransition(this, from, getTo(), text);
return t;
}
......
......@@ -69,7 +69,6 @@ import spins.promela.compiler.automaton.Automaton;
import spins.promela.compiler.automaton.ElseTransition;
import spins.promela.compiler.automaton.EndTransition;
import spins.promela.compiler.automaton.GotoTransition;
import spins.promela.compiler.automaton.NeverEndTransition;
import spins.promela.compiler.automaton.State;
import spins.promela.compiler.automaton.Transition;
import spins.promela.compiler.automaton.UselessTransition;
......@@ -514,14 +513,13 @@ public class LTSminTreeWalker {
else
newNextState = new State(p.getAutomaton(), next.isInAtomic());
Transition newTrans =
(trans instanceof ActionTransition ? new ActionTransition(newState, newNextState) :
(trans instanceof ElseTransition ? new ElseTransition(newState, newNextState) :
(trans instanceof EndTransition ? new EndTransition(newState) :
(trans instanceof NeverEndTransition ? new NeverEndTransition(newState) :
(trans instanceof GotoTransition ? new GotoTransition(newState, newNextState, trans.getText().substring(5)) :
(trans instanceof UselessTransition ? new UselessTransition(newState, newNextState, trans.getText()) :
null))))));
newTrans.setLabels(trans.getLabels());
(trans instanceof ActionTransition ? new ActionTransition(trans, newState, newNextState) :
(trans instanceof ElseTransition ? new ElseTransition(trans, newState, newNextState) :
(trans instanceof EndTransition ? new EndTransition(trans, newState) :
(trans instanceof GotoTransition ? new GotoTransition(trans, newState, newNextState, trans.getText().substring(5)) :
(trans instanceof UselessTransition ? new UselessTransition(trans, newState, newNextState, trans.getText()) :
null)))));
// Transition newTrans = trans.duplicateFrom(newState);
for (Action a : trans)
newTrans.addAction(instantiate(a, newTrans, p, null));
instantiate(next, newNextState, seen, p);
......@@ -1044,7 +1042,10 @@ public class LTSminTreeWalker {
/**
* Executed in the edge backtrack of the DFS to collect reachable atomic
* transitions .
* transitions.
*
* TODO: fix transitive closure calculation: states in an SCC have identical
* reachability properties (use Tarjan algorithm in atomic regions)
*/
private void annotate(LTSminTransition lt, LTSminState begin,
LTSminState end) {
......@@ -1109,7 +1110,7 @@ public class LTSminTreeWalker {
}
addSpecialGuards(lt, t, p); // proc die order && provided condition
createEnabledGuard(t, lt); // enabled action or else transition
if (lt.isNeverExecutable()) {
debug.say(MessageKind.NORMAL, "Removing dead transition "+ t +" of process "+ t.getProc());
continue; // skip dead transitions
......
......@@ -933,7 +933,7 @@ void never(): {
<LCURLY> s=sequence(currentProc.getStartState(), null, false) <RCURLY>
{
if(s != null) {
new NeverEndTransition(s);
new EndTransition(s);
}
setGotos();
currentProc = null;
......
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