← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/model/tapn/TimeInvariant.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/model/tapn/TimeInvariant.java
 
1
package dk.aau.cs.model.tapn;
 
2
 
 
3
import java.math.BigDecimal;
 
4
import java.util.Map;
 
5
import java.util.regex.Matcher;
 
6
import java.util.regex.Pattern;
 
7
 
 
8
import dk.aau.cs.model.tapn.Bound.InfBound;
 
9
import dk.aau.cs.util.Require;
 
10
 
 
11
public class TimeInvariant {
 
12
        public static final TimeInvariant LESS_THAN_INFINITY = new TimeInvariant(false, Bound.Infinity);
 
13
        private boolean isUpperIncluded;
 
14
        private Bound upper;
 
15
 
 
16
        public TimeInvariant(boolean isUpperIncluded, Bound upper) {
 
17
                Require.that(upper != null, "bound cannot be null");
 
18
                Require.that(isUpperIncluded || (!isUpperIncluded && upper.value() != 0), "\"< 0\" is and invalid invariant.");
 
19
                Require.that(upper != Bound.Infinity || !isUpperIncluded, "\"<=inf\" is not a valid invariant");
 
20
                
 
21
                this.isUpperIncluded = isUpperIncluded;
 
22
                this.upper = upper;
 
23
        }
 
24
 
 
25
        public Bound upperBound() {
 
26
                return upper;
 
27
        }
 
28
 
 
29
        public boolean isUpperNonstrict() {
 
30
                return isUpperIncluded;
 
31
        }
 
32
 
 
33
 
 
34
        public boolean isSatisfied(BigDecimal age) {
 
35
                if (upper instanceof InfBound)
 
36
                        return true;
 
37
                int comparison = age.compareTo(new BigDecimal(upper.value()));
 
38
 
 
39
                return isUpperIncluded ? comparison <= 0 : comparison < 0;
 
40
        }
 
41
 
 
42
        public static TimeInvariant parse(String invariant,
 
43
                        Map<String, Constant> constants) {
 
44
                Pattern pattern = Pattern.compile("^(<|<=)\\s*(\\w+)$");
 
45
                Matcher matcher = pattern.matcher(invariant);
 
46
                matcher.find();
 
47
 
 
48
                String operator = matcher.group(1);
 
49
                String boundAsString = matcher.group(2);
 
50
 
 
51
                if (operator.equals("<") && boundAsString.equals("0"))
 
52
                        return null;
 
53
                if (operator.equals("<=") && boundAsString.equals("inf"))
 
54
                        return null;
 
55
 
 
56
                Bound bound = null;
 
57
                if (boundAsString.equals("inf"))
 
58
                        bound = Bound.Infinity;
 
59
                else {
 
60
                        try {
 
61
                                int intBound = Integer.parseInt(boundAsString);
 
62
                                bound = new IntBound(intBound);
 
63
                        } catch (NumberFormatException e) {
 
64
                                if (constants.containsKey(boundAsString)) {
 
65
                                        bound = new ConstantBound(constants.get(boundAsString));
 
66
                                } else
 
67
                                        throw new RuntimeException("A constant which was not declared was used in an invariant.");
 
68
                        }
 
69
                }
 
70
 
 
71
                return new TimeInvariant(operator.equals("<="), bound);
 
72
        }
 
73
        
 
74
        public TimeInvariant copy() {
 
75
                return new TimeInvariant(this.isUpperIncluded, upper.copy());
 
76
        }
 
77
 
 
78
        @Override
 
79
        public String toString() {
 
80
                StringBuffer buffer = new StringBuffer();
 
81
                buffer.append(isUpperIncluded ? "<=" : "<");
 
82
                buffer.append(" ");
 
83
                buffer.append(upper);
 
84
                return buffer.toString();
 
85
        };
 
86
        
 
87
        public String toString(boolean displayConstantNames) {
 
88
                StringBuffer buffer = new StringBuffer();
 
89
                buffer.append(isUpperIncluded ? "<=" : "<");
 
90
                buffer.append(" ");
 
91
                buffer.append(displayConstantNames || upper instanceof InfBound ? upper : upper.value());
 
92
                return buffer.toString();
 
93
        }
 
94
 
 
95
        
 
96
        @Override
 
97
        public int hashCode() {
 
98
                final int prime = 31;
 
99
                int result = 1;
 
100
                result = prime * result + (isUpperIncluded ? 1231 : 1237);
 
101
                result = prime * result + ((upper == null) ? 0 : upper.hashCode());
 
102
                return result;
 
103
        }
 
104
 
 
105
        @Override
 
106
        public boolean equals(Object obj) {
 
107
                if (this == obj)
 
108
                        return true;
 
109
                if (obj == null)
 
110
                        return false;
 
111
                if (!(obj instanceof TimeInvariant))
 
112
                        return false;
 
113
                TimeInvariant other = (TimeInvariant) obj;
 
114
                if (isUpperIncluded != other.isUpperIncluded)
 
115
                        return false;
 
116
                if (upper == null) {
 
117
                        if (other.upper != null)
 
118
                                return false;
 
119
                } else if (!upper.equals(other.upper))
 
120
                        return false;
 
121
                return true;
 
122
        }
 
123
 
 
124
}