← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/verification/UPPAAL/VerifytaTraceInterpreter.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/verification/UPPAAL/VerifytaTraceInterpreter.java
5
5
import java.util.Iterator;
6
6
import java.util.List;
7
7
 
8
 
import dk.aau.cs.TA.trace.Participant;
9
 
import dk.aau.cs.TA.trace.TAFiringAction;
10
 
import dk.aau.cs.TA.trace.TimeDelayFiringAction;
11
 
import dk.aau.cs.TA.trace.TransitionFiring;
12
 
import dk.aau.cs.TA.trace.UppaalTrace;
13
 
import dk.aau.cs.petrinet.TAPNPlace;
14
 
import dk.aau.cs.petrinet.TAPNTransition;
15
 
import dk.aau.cs.petrinet.TimedArcPetriNet;
16
 
import dk.aau.cs.petrinet.Token;
17
 
import dk.aau.cs.petrinet.trace.TAPNFiringAction;
18
 
import dk.aau.cs.petrinet.trace.TAPNTrace;
 
8
import dk.aau.cs.model.NTA.trace.Participant;
 
9
import dk.aau.cs.model.NTA.trace.TAFiringAction;
 
10
import dk.aau.cs.model.NTA.trace.TimeDelayFiringAction;
 
11
import dk.aau.cs.model.NTA.trace.TransitionFiring;
 
12
import dk.aau.cs.model.NTA.trace.UppaalTrace;
 
13
import dk.aau.cs.model.tapn.TimedArcPetriNet;
 
14
import dk.aau.cs.model.tapn.TimedPlace;
 
15
import dk.aau.cs.model.tapn.TimedToken;
 
16
import dk.aau.cs.model.tapn.TimedTransition;
 
17
import dk.aau.cs.model.tapn.simulation.TimeDelayStep;
 
18
import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
 
19
import dk.aau.cs.model.tapn.simulation.TimedTransitionStep;
19
20
import dk.aau.cs.translations.TranslationNamingScheme;
20
21
import dk.aau.cs.translations.TranslationNamingScheme.TransitionTranslation;
21
22
import dk.aau.cs.translations.TranslationNamingScheme.TransitionTranslation.SequenceInfo;
24
25
        private final TimedArcPetriNet tapn;
25
26
        private final TranslationNamingScheme namingScheme;
26
27
 
27
 
        public VerifytaTraceInterpreter(TimedArcPetriNet tapn, TranslationNamingScheme namingScheme){
28
 
                this.tapn = tapn;
 
28
        public VerifytaTraceInterpreter(TimedArcPetriNet model, TranslationNamingScheme namingScheme) {
 
29
                this.tapn = model;
29
30
                this.namingScheme = namingScheme;
30
31
        }
31
32
 
32
 
        protected TimedArcPetriNet tapn(){
 
33
        protected TimedArcPetriNet tapn() {
33
34
                return tapn;
34
35
        }
35
36
 
36
 
        protected TranslationNamingScheme namingScheme(){
 
37
        protected TranslationNamingScheme namingScheme() {
37
38
                return namingScheme;
38
39
        }
39
40
 
40
 
        public TAPNTrace interpretTrace(UppaalTrace trace){
 
41
        public TimedArcPetriNetTrace interpretTrace(UppaalTrace trace) {
41
42
                return interpretTimedTrace(trace);
42
43
        }
43
44
 
44
 
        private TAPNTrace interpretTimedTrace(UppaalTrace trace) {
 
45
        private TimedArcPetriNetTrace interpretTimedTrace(UppaalTrace trace) {
45
46
                boolean isConcreteTrace = trace.isConcreteTrace();
46
 
                TAPNTrace result = new TAPNTrace(isConcreteTrace);
 
47
                TimedArcPetriNetTrace result = new TimedArcPetriNetTrace(isConcreteTrace);
47
48
 
48
49
                Iterator<TAFiringAction> iterator = trace.iterator();
49
50
                TAFiringAction action = null;
50
 
                
51
 
                while(iterator.hasNext()){
 
51
 
 
52
                while (iterator.hasNext()) {
52
53
                        List<TransitionFiring> firingSequence = new ArrayList<TransitionFiring>();
53
54
                        List<String> firingSequenceNames = new ArrayList<String>();
54
55
 
55
 
                        while(iterator.hasNext() && 
56
 
                                        (action = iterator.next()) instanceof TransitionFiring){
57
 
                                firingSequence.add((TransitionFiring)action);
58
 
                                firingSequenceNames.add(((TransitionFiring)action).channel());
 
56
                        while (iterator.hasNext() && (action = iterator.next()) instanceof TransitionFiring) {
 
57
                                firingSequence.add((TransitionFiring) action);
 
58
                                firingSequenceNames.add(((TransitionFiring) action).channel());
59
59
                        }
60
60
 
61
61
                        TransitionTranslation[] transitions = namingScheme.interpretTransitionSequence(firingSequenceNames);
62
62
 
63
 
                        for(TransitionTranslation transitionTranslation : transitions){
64
 
                                TAPNFiringAction firingAction = interpretTransitionFiring(firingSequence, transitionTranslation, isConcreteTrace);
65
 
                                result.addFiringAction(firingAction);
 
63
                        for (TransitionTranslation transitionTranslation : transitions) {
 
64
                                TimedTransitionStep transitionStep = interpretTransitionFiring(firingSequence, transitionTranslation, isConcreteTrace);
 
65
                                result.add(transitionStep);
66
66
                        }
67
67
 
68
 
 
69
 
                        if(action != null && action instanceof TimeDelayFiringAction){
70
 
                                BigDecimal delay = ((TimeDelayFiringAction)action).getDelay();
71
 
                                TAPNFiringAction delayAction = new dk.aau.cs.petrinet.trace.TimeDelayFiringAction(delay);
72
 
                                result.addFiringAction(delayAction);
 
68
                        if (action != null && action instanceof TimeDelayFiringAction) {
 
69
                                BigDecimal delay = ((TimeDelayFiringAction) action).getDelay();
 
70
                                TimeDelayStep delayAction = new TimeDelayStep(delay);
 
71
                                result.add(delayAction);
73
72
                        }
74
73
                }
75
74
 
76
75
                return result;
77
76
        }
78
77
 
79
 
        protected TAPNFiringAction interpretTransitionFiring
80
 
        (
81
 
                        List<TransitionFiring> firingSequence,
82
 
                        TransitionTranslation transitionTranslation,
83
 
                        boolean isConcreteTrace
84
 
        ) {
85
 
                TAPNTransition transition = tapn.getTransitionsByName(transitionTranslation.originalTransitionName());
86
 
                List<Token> tokens = null;
87
 
                if(isConcreteTrace){
88
 
                        if(transitionTranslation.sequenceInfo().equals(SequenceInfo.WHOLE)){
89
 
                                tokens = parseConsumedTokens(
90
 
                                                firingSequence.subList(transitionTranslation.startsAt(), transitionTranslation.endsAt()+1)
91
 
                                );
92
 
                        }else if(transitionTranslation.sequenceInfo().equals(SequenceInfo.END)){
 
78
        protected TimedTransitionStep interpretTransitionFiring(List<TransitionFiring> firingSequence,  TransitionTranslation transitionTranslation, boolean isConcreteTrace) {
 
79
                TimedTransition transition = tapn.getTransitionByName(transitionTranslation.originalTransitionName());
 
80
                List<TimedToken> tokens = null;
 
81
                if (isConcreteTrace) {
 
82
                        if (transitionTranslation.sequenceInfo().equals(SequenceInfo.WHOLE)) {
 
83
                                tokens = parseConsumedTokens(firingSequence.subList(transitionTranslation.startsAt(), transitionTranslation.endsAt() + 1));
 
84
                        } else if (transitionTranslation.sequenceInfo().equals(SequenceInfo.END)) {
93
85
                                TransitionFiring start = firingSequence.get(transitionTranslation.startsAt());
94
86
                                TransitionFiring end = firingSequence.get(transitionTranslation.endsAt());
95
87
                                tokens = parseConsumedTokens(start, end);
96
88
                        }
97
89
                }
98
90
 
99
 
                return new dk.aau.cs.petrinet.trace.TransitionFiringAction(transition, tokens);
 
91
                return new TimedTransitionStep(transition,tokens);
100
92
        }
101
93
 
102
 
        private List<Token> parseConsumedTokens(List<TransitionFiring> actions) {
103
 
                ArrayList<Token> tokens = new ArrayList<Token>();
 
94
        private List<TimedToken> parseConsumedTokens(List<TransitionFiring> actions) {
 
95
                ArrayList<TimedToken> tokens = new ArrayList<TimedToken>();
104
96
 
105
 
                for(int i = 0; i < actions.size(); i++){
 
97
                for (int i = 0; i < actions.size(); i++) {
106
98
                        TransitionFiring action = actions.get(i);
107
99
 
108
 
                        for(Participant participant : action.participants()){
 
100
                        for (Participant participant : action.participants()) {
109
101
                                String automata = participant.automata();
110
102
                                String sourceLocation = participant.location();
111
103
 
112
 
                                if(!namingScheme.isIgnoredAutomata(automata) && !namingScheme.isIgnoredPlace(sourceLocation)){
113
 
                                        TAPNPlace place = tapn.getPlaceByName(sourceLocation);
 
104
                                if (!namingScheme.isIgnoredAutomata(automata) && !namingScheme.isIgnoredPlace(sourceLocation)) {
 
105
                                        TimedPlace place = tapn.getPlaceByName(sourceLocation);
114
106
                                        BigDecimal clockValue = participant.clockOrVariableValue(namingScheme().tokenClockName()).lower();
115
 
                                        Token token = new Token(place, clockValue); 
 
107
                                        TimedToken token = new TimedToken(place, clockValue);
116
108
                                        tokens.add(token);
117
109
                                }
118
110
                        }
121
113
                return tokens;
122
114
        }
123
115
 
124
 
        private List<Token> parseConsumedTokens(TransitionFiring start, TransitionFiring end) {
125
 
                ArrayList<Token> tokens = new ArrayList<Token>();
 
116
        private List<TimedToken> parseConsumedTokens(TransitionFiring start, TransitionFiring end) {
 
117
                ArrayList<TimedToken> tokens = new ArrayList<TimedToken>();
126
118
 
127
 
                for(Participant participant : end.participants()){
 
119
                for (Participant participant : end.participants()) {
128
120
                        String automata = participant.automata();
129
121
                        String sourceLocation = start.sourceState().locationFor(automata);
130
122
 
131
 
                        if(!namingScheme.isIgnoredAutomata(automata) && !namingScheme.isIgnoredPlace(sourceLocation)){
132
 
                                TAPNPlace place = tapn.getPlaceByName(sourceLocation);
 
123
                        if (!namingScheme.isIgnoredAutomata(automata) && !namingScheme.isIgnoredPlace(sourceLocation)) {
 
124
                                TimedPlace place = tapn.getPlaceByName(sourceLocation);
133
125
                                BigDecimal clockValue = start.sourceState().getLocalClockOrVariable(automata, namingScheme().tokenClockName()).lower();
134
 
                                Token token = new Token(place, clockValue); 
 
126
                                TimedToken token = new TimedToken(place, clockValue);
135
127
                                tokens.add(token);
136
128
                        }
137
129
                }