← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/KBoundAnalyzer.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/pipe/gui/KBoundAnalyzer.java
1
1
package pipe.gui;
2
2
 
3
 
import pipe.dataLayer.DataLayer;
4
3
import pipe.dataLayer.TAPNQuery.SearchOption;
5
4
import pipe.dataLayer.TAPNQuery.TraceOption;
6
5
import pipe.gui.widgets.RunningVerificationDialog;
8
7
import dk.aau.cs.TCTL.TCTLAbstractProperty;
9
8
import dk.aau.cs.TCTL.TCTLAtomicPropositionNode;
10
9
import dk.aau.cs.TCTL.TCTLEFNode;
11
 
import dk.aau.cs.petrinet.PipeTapnToAauTapnTransformer;
12
 
import dk.aau.cs.petrinet.TAPN;
13
 
import dk.aau.cs.petrinet.TAPNQuery;
14
 
import dk.aau.cs.petrinet.colors.ColoredPipeTapnToColoredAauTapnTransformer;
 
10
import dk.aau.cs.model.tapn.TAPNQuery;
 
11
import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
15
12
import dk.aau.cs.translations.ReductionOption;
16
13
import dk.aau.cs.verification.ModelChecker;
17
14
import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
18
15
 
19
 
public class KBoundAnalyzer 
20
 
{
21
 
        protected DataLayer appModel;
 
16
public class KBoundAnalyzer {
 
17
        protected TimedArcPetriNetNetwork tapnNetwork;
22
18
        protected int k;
23
19
 
24
20
        private ModelChecker modelChecker;
25
21
        private Messenger messenger;
26
22
 
27
 
        public KBoundAnalyzer(DataLayer appModel, int k, ModelChecker modelChecker, Messenger messenger)
28
 
        {
 
23
        public KBoundAnalyzer(TimedArcPetriNetNetwork tapnNetwork, int k,
 
24
                        ModelChecker modelChecker, Messenger messenger) {
29
25
                this.k = k;
30
 
                this.appModel = appModel;
 
26
                this.tapnNetwork = tapnNetwork;
31
27
                this.modelChecker = modelChecker;
32
28
                this.messenger = messenger;
33
29
        }
36
32
                return new RunKBoundAnalysis(modelChecker, messenger);
37
33
        }
38
34
 
39
 
        public void analyze()
40
 
        {
41
 
                TAPN model = convertModelToAAUTAPN(appModel);
42
 
                TAPNQuery query = getBoundednessQuery(model.getNumberOfTokens());
 
35
        public void analyze() {
 
36
                TAPNQuery query = getBoundednessQuery();
43
37
                VerifytaOptions options = verificationOptions();
44
38
 
45
39
                RunKBoundAnalysis analyzer = getAnalyzer(modelChecker, messenger);
46
 
                RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());   
 
40
                RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
47
41
                dialog.setupListeners(analyzer);
48
42
 
49
 
                analyzer.execute(options, model, query);
 
43
                analyzer.execute(options, tapnNetwork, query);
50
44
                dialog.setVisible(true);
51
45
        }
52
46
 
54
48
                return new VerifytaOptions(TraceOption.NONE, SearchOption.BFS, false, ReductionOption.KBOUNDANALYSIS);
55
49
        }
56
50
 
57
 
        private TAPN convertModelToAAUTAPN(DataLayer appModel) {
58
 
                PipeTapnToAauTapnTransformer transformer = appModel.isUsingColors() ? new ColoredPipeTapnToColoredAauTapnTransformer() : new PipeTapnToAauTapnTransformer();
59
 
 
60
 
                TAPN model=null;
61
 
                try {
62
 
                        model = transformer.getAAUTAPN(appModel, 0);
63
 
                } catch (Exception e) {
64
 
                        e.printStackTrace();
65
 
                }
66
 
                return model;
67
 
        }
68
 
 
69
 
        protected TAPNQuery getBoundednessQuery(int tokensInModel) {
 
51
        protected TAPNQuery getBoundednessQuery() {
70
52
                TCTLAbstractProperty property = null;
71
53
 
72
 
                property = new TCTLEFNode(
73
 
                                new TCTLAtomicPropositionNode("P_capacity", "=", 0)
74
 
                );              
75
 
 
76
 
 
77
 
                return new TAPNQuery(property, k + 1 + tokensInModel);
 
54
                property = new TCTLEFNode(new TCTLAtomicPropositionNode("_BOTTOM_", "=", 0));
 
55
 
 
56
                return new TAPNQuery(property, k + 1);
78
57
        }
79
58
}