Skip to content

Commit 43ed5db

Browse files
yanntmyanntm
authored
Merge pull request #4 from lip6/master
merge
2 parents 257ab3d + 279d4a1 commit 43ed5db

File tree

165 files changed

+18970
-1459
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

165 files changed

+18970
-1459
lines changed

‎.github/workflows/build.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,5 +39,5 @@ jobs:
3939
# You should create a personal access token and store it in your repository
4040
token: ${{ secrets.NOTIF_PAT }}
4141
repo: ITS-commandline
42-
owner: bnslmn
42+
owner: yanntm
4343
event_type: rebuild

‎fr.lip6.move.gal.parent/pom.xml

+5
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,11 @@
8484

8585
<module>../pins/fr.lip6.move.gal.gal2pins</module>
8686
<module>../pnmcc/fr.lip6.move.gal.pn2pins</module>
87+
88+
<!-- LTL related functionality -->
89+
<module>../ltl/fr.lip6.ltl.jhoaf</module>
90+
<module>../ltl/fr.lip6.ltl.tgba</module>
91+
8792
<!-- LTSmin interactions : launching and configuration -->
8893
<module>../ltsmin/fr.lip6.move.gal.ltsmin.preference</module>
8994
<module>../ltsmin/fr.lip6.move.gal.ltsmin.binaries</module>

‎fr.lip6.move.gal.structural/build.properties

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
source.. = src/
22
output.. = bin/
3-
bin.includes = plugin.xml,\
4-
META-INF/,\
3+
bin.includes = META-INF/,\
54
.

‎fr.lip6.move.gal.structural/plugin.xml

-5
This file was deleted.

‎fr.lip6.move.gal.structural/src/android/util/SparseArray.java

+19
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,25 @@ public E get(int key, E valueIfKeyNotFound) {
107107
return (E) mValues[i];
108108
}
109109
}
110+
111+
/**
112+
* Delete an element at index and shift elements to the right by one.
113+
* @param i
114+
*/
115+
public void deleteAndShift(int i) {
116+
if (mSize==0 || i > mKeys[mSize-1]) {
117+
return;
118+
}
119+
int k;
120+
for (k= mSize-1 ; k>=0 && mKeys[k]>i ; k--) {
121+
mKeys[k]--;
122+
}
123+
if (k >= 0 && mKeys[k]==i) {
124+
removeAt(k);
125+
}
126+
}
127+
128+
110129
/**
111130
* Removes the mapping from the specified key, if there was any.
112131
*/

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/ConcurrentHashDoneProperties.java

-2
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,5 @@ public Set<String> keySet() {
3737
public int size() {
3838
return map.size();
3939
}
40-
41-
4240

4341
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropHandler.java

+3-3
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@
1212
import org.xml.sax.SAXException;
1313
import org.xml.sax.helpers.DefaultHandler;
1414

15+
import fr.lip6.move.gal.structural.ISparsePetriNet;
1516
import fr.lip6.move.gal.structural.PetriNet;
1617
import fr.lip6.move.gal.structural.Property;
17-
import fr.lip6.move.gal.structural.SparsePetriNet;
1818
import fr.lip6.move.gal.structural.expr.Expression;
1919
import fr.lip6.move.gal.structural.expr.NaryOp;
2020
import fr.lip6.move.gal.structural.expr.Op;
@@ -229,8 +229,8 @@ public void popBinary(Op op) {
229229

230230
private Map<String,Integer> tcache = null;
231231
private int findTransition(String name) {
232-
if (spec instanceof SparsePetriNet) {
233-
SparsePetriNet spn = (SparsePetriNet) spec;
232+
if (spec instanceof ISparsePetriNet) {
233+
ISparsePetriNet spn = (ISparsePetriNet) spec;
234234
if (tcache == null) {
235235
// no reindex https://stackoverflow.com/questions/434989/hashmap-initialization-parameters-load-initialcapacity
236236
tcache = new HashMap<> ( (spn.getTnames().size() *4+2)/3 );

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/mcc/properties/PropertiesToPNML.java

+8-1
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,12 @@
66
import java.util.Map;
77
import java.util.logging.Logger;
88

9+
import fr.lip6.move.gal.structural.ISparsePetriNet;
910
import fr.lip6.move.gal.structural.Property;
1011
import fr.lip6.move.gal.structural.PropertyType;
1112
import fr.lip6.move.gal.structural.SparsePetriNet;
1213
import fr.lip6.move.gal.structural.expr.ArrayVarRef;
14+
import fr.lip6.move.gal.structural.expr.AtomicPropRef;
1315
import fr.lip6.move.gal.structural.expr.BinOp;
1416
import fr.lip6.move.gal.structural.expr.BoolConstant;
1517
import fr.lip6.move.gal.structural.expr.Constant;
@@ -75,7 +77,7 @@ public static boolean transform(SparsePetriNet spn, String path, DoneProperties
7577
}
7678

7779

78-
private static boolean exportProperty(PrintWriter pw, Expression body, PropertyType type, SparsePetriNet spn) {
80+
private static boolean exportProperty(PrintWriter pw, Expression body, PropertyType type, ISparsePetriNet spn) {
7981
if (body == null) {
8082
return false;
8183
} else if (type == PropertyType.DEADLOCK) {
@@ -394,4 +396,9 @@ public Void visit(NaryOp naryOp) {
394396
}
395397
return null;
396398
}
399+
400+
@Override
401+
public Void visit(AtomicPropRef apRef) {
402+
return apRef.getAp().getExpression().accept(this);
403+
}
397404
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/DeadlockFound.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package fr.lip6.move.gal.structural;
22

3-
public class DeadlockFound extends Exception {
3+
public class DeadlockFound extends GlobalPropertySolvedException {
44

55
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/FlowDimacsPrinter.java

+3-3
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,15 @@
77
import java.util.List;
88

99
import android.util.SparseIntArray;
10-
import fr.lip6.move.gal.util.MatrixCol;
10+
import fr.lip6.move.gal.util.IntMatrixCol;
1111

1212
public class FlowDimacsPrinter {
1313

1414
public static String drawNet (StructuralReduction sr) {
1515
return drawNet(sr.getFlowPT(),sr.getFlowTP(),sr.getMarks(),sr.getPnames(),sr.getTnames());
1616
}
1717

18-
public static String drawNet (MatrixCol flowPT, MatrixCol flowTP, List<Integer> marks, List<String> pnames, List<String> tnames) {
18+
public static String drawNet (IntMatrixCol flowPT, IntMatrixCol flowTP, List<Integer> marks, List<String> pnames, List<String> tnames) {
1919
try {
2020
long time = System.currentTimeMillis();
2121
Path out = Files.createTempFile("petri", ".sym");
@@ -137,7 +137,7 @@ public static String drawNet (MatrixCol flowPT, MatrixCol flowTP, List<Integer>
137137
return null;
138138
}
139139

140-
private static long countNonTrivial(MatrixCol flowPT) {
140+
private static long countNonTrivial(IntMatrixCol flowPT) {
141141
long nontrivialedge = 0;
142142
for (SparseIntArray sa : flowPT.getColumns()) {
143143
for (int i=0;i<sa.size(); i++) {

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/FlowMatrix.java

+13-13
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,21 @@
11
package fr.lip6.move.gal.structural;
22

33
import android.util.SparseIntArray;
4-
import fr.lip6.move.gal.util.MatrixCol;
4+
import fr.lip6.move.gal.util.IntMatrixCol;
55

66
public class FlowMatrix {
77
// To represent the flow matrix, if we can build it. We use a sparse representation.
88
// Map variable index -> Transition index -> update to variable (a relative integer)
9-
private MatrixCol flow ;
10-
private MatrixCol read ;
11-
private MatrixCol flowPT ;
12-
private MatrixCol flowTP ;
9+
private IntMatrixCol flow ;
10+
private IntMatrixCol read ;
11+
private IntMatrixCol flowPT ;
12+
private IntMatrixCol flowTP ;
1313

1414
public FlowMatrix (int nbvar, int nbtrans) {
15-
flow = new MatrixCol(nbvar, nbtrans);
16-
flowPT = new MatrixCol(nbvar, nbtrans);
17-
flowTP = new MatrixCol(nbvar, nbtrans);
18-
read = new MatrixCol(nbvar, nbtrans);
15+
flow = new IntMatrixCol(nbvar, nbtrans);
16+
flowPT = new IntMatrixCol(nbvar, nbtrans);
17+
flowTP = new IntMatrixCol(nbvar, nbtrans);
18+
read = new IntMatrixCol(nbvar, nbtrans);
1919
}
2020

2121
public void addWriteEffect(int tindex, int vindex, int val) {
@@ -46,19 +46,19 @@ public void addReadEffect(int tindex, int vindex, int val) {
4646
read.getColumn(tindex).put(vindex, max);
4747
}
4848

49-
public MatrixCol getIncidenceMatrix() {
49+
public IntMatrixCol getIncidenceMatrix() {
5050
return flow;
5151
}
5252

53-
public MatrixCol getRead() {
53+
public IntMatrixCol getRead() {
5454
return read;
5555
}
5656

57-
public MatrixCol getFlowPT() {
57+
public IntMatrixCol getFlowPT() {
5858
return flowPT;
5959
}
6060

61-
public MatrixCol getFlowTP() {
61+
public IntMatrixCol getFlowTP() {
6262
return flowTP;
6363
}
6464

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/FlowPrinter.java

+6-6
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
import java.util.Set;
1313

1414
import android.util.SparseIntArray;
15-
import fr.lip6.move.gal.util.MatrixCol;
15+
import fr.lip6.move.gal.util.IntMatrixCol;
1616

1717
public class FlowPrinter {
1818

@@ -31,10 +31,10 @@ public static String drawNet (StructuralReduction sr, String title, Set<Integer>
3131
return drawNet(sr, title, hlPlaces, hlTrans, 200);
3232
}
3333
public static String drawNet (StructuralReduction sr, String title, Set<Integer> hlPlaces, Set<Integer> hlTrans, int maxShown) {
34-
return drawNet(sr.getFlowPT(),sr.getFlowTP(),sr.getMarks(),sr.getPnames(),sr.getTnames(), sr.getUntouchable(), "places: "+sr.getPnames().size() + " trans:"+ sr.getTnames().size()+ " " + title, hlPlaces, hlTrans, maxShown);
34+
return drawNet(sr.getFlowPT(),sr.getFlowTP(),sr.getMarks(),sr.getPnames(),sr.getTnames(), sr.computeSupport(), "places: "+sr.getPnames().size() + " trans:"+ sr.getTnames().size()+ " " + title, hlPlaces, hlTrans, maxShown);
3535
}
3636

37-
public static String drawNet (MatrixCol flowPT, MatrixCol flowTP, List<Integer> marks, List<String> pnames, List<String> tnames, BitSet untouchable, String title, Set<Integer> hlPlaces, Set<Integer> hlTrans, int maxShown) {
37+
public static String drawNet (IntMatrixCol flowPT, IntMatrixCol flowTP, List<Integer> marks, List<String> pnames, List<String> tnames, BitSet untouchable, String title, Set<Integer> hlPlaces, Set<Integer> hlTrans, int maxShown) {
3838
try {
3939
Path out = Files.createTempFile("petri"+nbWritten++ +"_", ".dot");
4040
PrintWriter pw = new PrintWriter(out.toFile());
@@ -46,8 +46,8 @@ public static String drawNet (MatrixCol flowPT, MatrixCol flowTP, List<Integer>
4646
Set<Integer> torep = new HashSet<>();
4747
Set<Integer> toret = new HashSet<>();
4848

49-
MatrixCol tflowPT = null;
50-
MatrixCol tflowTP = null;
49+
IntMatrixCol tflowPT = null;
50+
IntMatrixCol tflowTP = null;
5151

5252
if (pnames.size() + tnames.size() > 2*maxShown) {
5353
isLarge = true;
@@ -190,7 +190,7 @@ public static String drawNet (MatrixCol flowPT, MatrixCol flowTP, List<Integer>
190190
return null;
191191
}
192192

193-
private static void addNeighborhood(int ti, MatrixCol flowPT, MatrixCol flowTP, Set<Integer> torep,
193+
private static void addNeighborhood(int ti, IntMatrixCol flowPT, IntMatrixCol flowTP, Set<Integer> torep,
194194
Set<Integer> toret) {
195195
toret.add(ti);
196196
SparseIntArray col = flowPT.getColumn(ti);

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/GlobalPropertySolvedException.java

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
package fr.lip6.move.gal.structural;
2+
3+
public class GlobalPropertySolvedException extends Exception {
4+
5+
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/ISparsePetriNet.java

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
package fr.lip6.move.gal.structural;
2+
3+
import java.util.BitSet;
4+
import java.util.List;
5+
6+
import fr.lip6.move.gal.util.IntMatrixCol;
7+
8+
public interface ISparsePetriNet {
9+
10+
List<Integer> getMarks();
11+
12+
IntMatrixCol getFlowTP();
13+
14+
IntMatrixCol getFlowPT();
15+
16+
int getPlaceCount();
17+
18+
int getTransitionCount();
19+
20+
List<String> getTnames();
21+
22+
List<String> getPnames();
23+
24+
int getMaxArcValue();
25+
26+
BitSet computeSupport();
27+
28+
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/InvariantCalculator.java

+3-3
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
import java.util.logging.Logger;
88

99
import android.util.SparseIntArray;
10-
import fr.lip6.move.gal.util.MatrixCol;
10+
import fr.lip6.move.gal.util.IntMatrixCol;
1111
import uniol.apt.analysis.invariants.InvariantCalculator.InvariantAlgorithm;
1212

1313
/**
@@ -75,11 +75,11 @@ public static void printInvariant (Collection<SparseIntArray> invariants, List<S
7575
System.out.println("Total of "+invariants.size() + " invariants.");
7676
}
7777

78-
public static Set<SparseIntArray> computePInvariants (MatrixCol pn, List<String> pnames) {
78+
public static Set<SparseIntArray> computePInvariants (IntMatrixCol pn, List<String> pnames) {
7979
return computePInvariants(pn, pnames,false);
8080
}
8181

82-
public static Set<SparseIntArray> computePInvariants (MatrixCol pn, List<String> pnames, boolean onlyPositive) {
82+
public static Set<SparseIntArray> computePInvariants (IntMatrixCol pn, List<String> pnames, boolean onlyPositive) {
8383
Set<SparseIntArray> invar ;
8484
long time = System.currentTimeMillis();
8585
try {

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/NoDeadlockExists.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
package fr.lip6.move.gal.structural;
22

3-
public class NoDeadlockExists extends Exception {
3+
public class NoDeadlockExists extends GlobalPropertySolvedException {
44

55
}

‎fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/Property.java

+3
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,9 @@ public Property(Expression prop, PropertyType type, String name) {
1313
}
1414
public Property() {
1515
}
16+
public Property copy () {
17+
return new Property(prop, type, name);
18+
}
1619
public void setName(String name) {
1720
this.name = name;
1821
}

0 commit comments

Comments
 (0)