Commit 229b353d authored by DEANTONI Julien's avatar DEANTONI Julien

fix state space construction. Defer is now working ok and bounded SDF

models are actually bounded :)
use hppc 0.6 since 7.2 is missing a class used by grph
parent f5ea10a5
......@@ -97,7 +97,7 @@ public abstract class AbstractRuntimeExpression extends AbstractConstraint
@Override
public void restoreState(SerializedConstraintState stateData) {
born = (Boolean) stateData.restore(0);
born = (boolean) stateData.restore(0);
state = State.values()[ (Integer) stateData.restore(1) ];
}
......
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
/**
*
*/
......@@ -27,7 +17,7 @@ import fr.inria.aoste.timesquare.ccslkernel.solver.statistics.SolverRuntimeStats
* @author jdeanton
*
*/
public class CCSLConstraintState extends HashMap<UniqueString, SerializedConstraintState> implements Serializable {
public class CCSLConstraintState extends HashMap<String, SerializedConstraintState> implements Serializable {
/**
* id for hypothetical serialization
......@@ -40,7 +30,7 @@ public class CCSLConstraintState extends HashMap<UniqueString, SerializedConstra
public void copy(CCSLConstraintState from){
this.clear();
for(UniqueString key : from.keySet()){
for(String key : from.keySet()){
SerializedConstraintState newList = new SerializedConstraintState(from.get(key));
this.put(key, newList);
}
......@@ -56,10 +46,10 @@ public class CCSLConstraintState extends HashMap<UniqueString, SerializedConstra
return false;
}
Iterator<Entry<UniqueString, SerializedConstraintState>> it = state1.entrySet().iterator();
Iterator<Entry<String, SerializedConstraintState>> it = state1.entrySet().iterator();
while(it.hasNext()){
Map.Entry<UniqueString, SerializedConstraintState> entry = (Map.Entry<UniqueString, SerializedConstraintState>) it.next();
UniqueString key = entry.getKey();
Map.Entry<String, SerializedConstraintState> entry = (Map.Entry<String, SerializedConstraintState>) it.next();
String key = entry.getKey();
if (! this.containsKey(key)){
if (CCSLKernelSolver.runtimeStatsCollection)
SolverRuntimeStats.leaveMethod(getClass().getName() + ".equals");
......
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
package fr.inria.aoste.timesquare.ccslkernel.explorer;
import java.io.IOException;
......
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
package fr.inria.aoste.timesquare.ccslkernel.explorer;
import org.eclipse.emf.common.util.EList;
......
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
package fr.inria.aoste.timesquare.ccslkernel.explorer;
import com.carrotsearch.hppc.cursors.IntCursor;
import grph.Grph;
import grph.oo.ObjectGrph;
import grph.path.Path;
public class StateSpace extends ObjectGrph<CCSLConstraintState, StringBuffer> {
......@@ -22,44 +9,4 @@ public class StateSpace extends ObjectGrph<CCSLConstraintState, StringBuffer> {
return this.backingGrph;
}
public int e2i(StringBuffer s){
return super.e2i(s);
}
public void changeEdgeColor(StringBuffer label, int color){
this.getGrph().getEdgeColorProperty().setValue(e2i(label), color);
this.getGrph().getEdgeWidthProperty().setValue(e2i(label), 3);
}
public void changeEdgeColorAndBig(StringBuffer label, int color){
this.getGrph().getEdgeColorProperty().setValue(e2i(label), color);
this.getGrph().getEdgeWidthProperty().setValue(e2i(label), 6);
}
public void changeVertexShape(CCSLConstraintState s, int shape){
this.getGrph().getVertexShapeProperty().setValue(v2i(s), shape);
}
public void changeVertexColor(CCSLConstraintState s, int c){
this.getGrph().getVertexColorProperty().setValue(v2i(s), c);
}
public Path getShortestPath(CCSLConstraintState source, CCSLConstraintState destination){
return getGrph().getShortestPath(v2i(source), v2i(destination));
}
public void ChangeSinkColor(int color){
for (IntCursor ic : this.getGrph().getSinks()){
this.getGrph().getVertexColorProperty().setValue(ic.value, 15);
}
}
public CCSLConstraintState i2v(int i){
return super.i2v(i);
}
public StringBuffer i2e(int i){
return super.i2e(i);
}
}
......@@ -1393,14 +1393,14 @@ public class CCSLKernelSolver {
for(ISolverConcrete concrete: clockInstantiationTree.lookupInstances(null)){
if (concrete instanceof SolverClock){
SolverClock clock = (SolverClock) concrete;
currentState.put(new UniqueString(clock.getInstantiatedElement().getQualifiedName()), clock.dumpState());
currentState.put(clock.getInstantiatedElement().getQualifiedName(), clock.dumpState());
}
}
for(ISolverConcrete concrete: elementInstantiationTree.lookupInstances(null)){
if (concrete instanceof SolverSequenceElement){
SolverSequenceElement seq = (SolverSequenceElement) concrete;
currentState.put(new UniqueString(seq.getInstantiatedElement().getQualifiedName()), seq.dumpState());
currentState.put(seq.getInstantiatedElement().getQualifiedName(), seq.dumpState());
}
}
......@@ -1408,15 +1408,15 @@ public class CCSLKernelSolver {
for(ISolverConcrete concrete : allConcreteElements){
if (concrete instanceof SolverExpression){
SolverExpression expr = (SolverExpression) concrete;
currentState.put(new UniqueString(expr.getInstantiatedElement().getQualifiedName()), expr.dumpState());
currentState.put(expr.getInstantiatedElement().getQualifiedName(), expr.dumpState());
}
if (concrete instanceof SolverRelation){
SolverRelation rel = (SolverRelation) concrete;
currentState.put(new UniqueString(rel.getInstantiatedElement().getQualifiedName()), rel.dumpState());
currentState.put(rel.getInstantiatedElement().getQualifiedName(), rel.dumpState());
}
if (concrete instanceof SolverRelationWrapper){
SolverRelationWrapper rel = (SolverRelationWrapper) concrete;
currentState.put(new UniqueString(rel.getInstantiatedElement().getQualifiedName()), rel.dumpState());
currentState.put(rel.getInstantiatedElement().getQualifiedName(), rel.dumpState());
}
}
return currentState;
......@@ -1424,13 +1424,13 @@ public class CCSLKernelSolver {
public void setCurrentState(CCSLConstraintState newState){
for(UniqueString concreteQN : newState.keySet()){
ISolverConcrete concrete = concreteInstantiationTree.lookupInstance(concreteQN.internalString);
for(String concreteQN : newState.keySet()){
ISolverConcrete concrete = concreteInstantiationTree.lookupInstance(concreteQN);
if(concrete == null){
concrete = elementInstantiationTree.lookupInstance(concreteQN.internalString);
concrete = elementInstantiationTree.lookupInstance(concreteQN);
}
if(concrete == null){
concrete = clockInstantiationTree.lookupInstance(concreteQN.internalString);
concrete = clockInstantiationTree.lookupInstance(concreteQN);
}
SerializedConstraintState concreteNewState = newState.get(concreteQN);
......@@ -1441,5 +1441,4 @@ public class CCSLKernelSolver {
}
......@@ -21,3 +21,5 @@ Require-Bundle: org.eclipse.ui,
Bundle-RequiredExecutionEnvironment: JavaSE-1.7
Bundle-ActivationPolicy: lazy
Bundle-Vendor: INRIA/I3S AOSTE
Export-Package: fr.inria.aoste.timesquare.explorer.ui,
fr.inria.aoste.timesquare.explorer.ui.popup.action
......@@ -3,7 +3,7 @@ digraph {
start=0;
node [style="filled"]
0 [fillcolor="#ffffff", size="10", shape="circle", fontcolor="black", label="1112653818"];
0 [fillcolor="#ffffff", size="10", shape="circle", fontcolor="black", label="2142718946"];
0 -> 0 [penwidth="1", color="#aaaaaa", style="solid", label="[c2, c1]"];
0 -> 0 [penwidth="1", color="#aaaaaa", style="solid", label="[c1, c2]"];
}
\ No newline at end of file
......@@ -16,7 +16,7 @@ ClockConstraintSystem MySpec {
Clock c2
Clock res
Sequence s1 : IntegerSequence = 3; 4; (3)
Sequence s1 : IntegerSequence = 3; 4; (3; 2)
Expression myDefer = Defer(BaseClock -> c1, DelayClock -> c2, DelayPatternExpression -> s1)
Relation r1[Coincides](Clock1 -> res, Clock2 -> myDefer)
}
......
......@@ -23,9 +23,9 @@ ClockConstraintSystem anSDFmodel {
Integer one=1
Integer two=2
Relation arcBtoA[Arc]( Arc_delay-> three,
Relation arcBtoA[Arc]( Arc_delay-> two,
Arc_source-> B,
Arc_outWeight->one,
Arc_outWeight->two,
Arc_target-> A,
Arc_inWeight-> one
)
......
/*
* the SDF MoCC Library
* @author: Julien Deantoni
* date : Sun September 04 2011 15:03:42 CEST
*/
Library SDF{
imports{
import "platform:/plugin/fr.inria.aoste.timesquare.ccslkernel.model/ccsllibrary/kernel.ccslLib" as kernel;
import "platform:/plugin/fr.inria.aoste.timesquare.ccslkernel.model/ccsllibrary/CCSL.ccslLib" as kernel;
}
RelationLibrary SDF_Relations{
/*
* Constraint associated with the token manipulation
*/
RelationDeclaration Token(Token_write:clock, Token_read:clock, Token_delay:int)
ConditionalRelationDefinition TokenDef[Token]{
Integer zero=0
Expression Token_readDelayedForDelay=DelayFor( DelayForClockToDelay-> Token_read,
DelayForClockForCounting-> Token_read,
DelayForDelay-> Token_delay
)
switch{
case IntInf{
leftValue IntegerVariableRef[Token_delay]
rightValue IntegerRef[one]
}:
Relation Token_causalityImmediate1[Causes](LeftClock-> Token_write, RightClock-> Token_read)
case IntSup{
leftValue IntegerVariableRef[Token_delay]
rightValue IntegerRef[zero]
}:
Relation Token_causalityImmediate2[Causes](LeftClock-> Token_write, RightClock-> Token_readDelayedForDelay)
}default Relation Token_causalityDelayed[Coincides](Clock1-> Token_write, Clock2-> Token_write)
}
/*
* Constraints associated to each input
*/
RelationDeclaration Input(Input_actor:clock, Input_read:clock, Input_weight:int)
RelationDefinition InputDef[Input]{
Sequence Input_ByWeight=(IntegerVariableRef[Input_weight])
Expression Input_readByWeight=FilterBy( FilterByClock->Input_read,
FilterBySeq-> Input_ByWeight
)
Relation Input_weightTokenCausesExec[Causes](LeftClock-> Input_readByWeight,
RightClock-> Input_actor
)
}
/*
* Constraints associated to each output
*/
RelationDeclaration Output(Output_actor:clock, Output_write:clock, Output_weight:int)
RelationDefinition OutputDef[Output]{
Sequence Output_ByWeight= 1 (IntegerVariableRef[Output_weight])
Expression Output_writeByWeight=FilterBy( FilterByClock->Output_write,
FilterBySeq-> Output_ByWeight
)
Relation Output_ExecWriteFirstToken[Coincides](Clock1-> Output_actor,
Clock2-> Output_writeByWeight
)
}
/*
* The arc relation is combining the other and can be the only one used to apply the MoCC
*/
RelationDeclaration Arc(Arc_delay:int,
Arc_source:clock,
Arc_outWeight:int,
Arc_target:clock,
Arc_inWeight:int
)
RelationDefinition ArcDef[Arc]{
//internal clocks
Clock Arc_Write:clock
Clock Arc_read:clock
Relation Arc_output[Output](Output_actor-> Arc_source,
Output_write-> Arc_Write,
Output_weight-> Arc_outWeight
)
Relation Arc_token[Token](Token_write-> Arc_Write,
Token_read-> Arc_read,
Token_delay-> Arc_delay
)
Relation Arc_input[Input](Input_actor-> Arc_target,
Input_read-> Arc_read,
Input_weight-> Arc_inWeight
)
}
}
}
\ No newline at end of file
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
package fr.inria.aoste.timesquare.trace.checker.ui.popup.action;
import java.io.IOException;
......@@ -117,19 +107,19 @@ public class CreateTraceSpecificStateSpace extends AbstractHandler {
}
private void cleanAndSerializeStateSpace() {
for(StringBuffer s : stateSpace.getEdges()){
if (!isContainingAnObservedClock(s.toString())){
s = new StringBuffer("");
for(UniqueString s : stateSpace.getEdges()){
if (!isContainingAnObservedClock(s.internalString)){
s.internalString = "";
stateSpace.getGrph().getEdgeLabelProperty().setValue(stateSpace.e2i(s), "");
}else{
//here it contains an observed clock
StringBuilder newLabel = new StringBuilder();
for(String clockName : s.toString().split(",")){
for(String clockName : s.internalString.split(",")){
if(isContainingAnObservedClock(clockName)){
newLabel.append(clockName);
}
}
s.append(newLabel.toString());
s.internalString = newLabel.toString();
stateSpace.getGrph().getEdgeLabelProperty().setValue(stateSpace.e2i(s), newLabel.toString());
}
}
......@@ -189,8 +179,8 @@ public class CreateTraceSpecificStateSpace extends AbstractHandler {
}
ArrayList<CCSLConstraintState> allPathToHighlight = new ArrayList<CCSLConstraintState>();
for (StringBuffer label : stateSpace.getEdges()) {
if (isContainingAnObservedClock(label.toString())){
for (UniqueString label : stateSpace.getEdges()) {
if (isContainingAnObservedClock(label.internalString)){
if(label.toString().contains("DEAD")){
stateSpace.changeEdgeColorAndBig(label, 7);
}else{
......
/*******************************************************************************
* Copyright (c) 2017 I3S laboratory, INRIA and others.
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Contributors:
* I3S laboratory and INRIA Kairos - initial API and implementation
*******************************************************************************/
package fr.inria.aoste.timesquare.trace.checker.ui.popup.action;
import java.io.IOException;
......@@ -16,7 +6,7 @@ import java.util.List;
import org.eclipse.core.resources.IFile;
//import com.sun.mail.imap.Quota.Resource;
import com.sun.mail.imap.Quota.Resource;
import toools.io.file.RegularFile;
import toools.set.IntSet;
......@@ -63,14 +53,14 @@ public class PathCCSLSpecificationGenerator {
currentV = ResultsHolder.maxPath.getVertexAt(i);
IntSet allConnectingEdges = null;
allConnectingEdges = stateSpace.getGrph().getEdgesConnecting(lastV, currentV);
StringBuffer oneEdge = stateSpace.i2e(allConnectingEdges.toIntArray()[0]);
if (oneEdge.toString().startsWith("[")){
oneEdge = new StringBuffer(oneEdge.toString().substring(1));
UniqueString oneEdge = stateSpace.i2e(allConnectingEdges.toIntArray()[0]);
if (oneEdge.internalString.startsWith("[")){
oneEdge.internalString = oneEdge.internalString.substring(1);
}
if (oneEdge.toString().endsWith("]")){
oneEdge = new StringBuffer(oneEdge.toString().substring(0, oneEdge.length()-1));
if (oneEdge.internalString.endsWith("]")){
oneEdge.internalString = oneEdge.internalString.substring(0, oneEdge.internalString.length()-1);
}
for(String clockName : oneEdge.toString().split(",")){
for(String clockName : oneEdge.internalString.split(",")){
res.add(clockName.replaceAll(" *", ""));
}
lastV = currentV;
......@@ -146,11 +136,11 @@ public class PathCCSLSpecificationGenerator {
currentV = ResultsHolder.maxPath.getVertexAt(i);
IntSet allConnectingEdges = null;
allConnectingEdges = stateSpace.getGrph().getEdgesConnecting(lastV, currentV);
StringBuffer oneEdge = stateSpace.i2e(allConnectingEdges.toIntArray()[0]);
UniqueString oneEdge = stateSpace.i2e(allConnectingEdges.toIntArray()[0]);
HashSet<String> allUniqueClocksToTrigger = new HashSet<String>();
StringBuilder allClocksToTrigger = new StringBuilder();
for(String s : oneEdge.toString().split(",")){
for(String s : oneEdge.internalString.split(",")){
s = s.replaceAll(" *", "");
s = s.replaceAll("\\[", "");
s = s.replaceAll("\\]", "");
......
......@@ -4,7 +4,7 @@
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry exported="true" kind="lib" path="code/grph-1.10.8.jar"/>
<classpathentry exported="true" kind="lib" path="code/hppc-0.7.2.jar"/>
<classpathentry exported="true" kind="lib" path="code/toools-0.1.8.jar"/>
<classpathentry exported="true" kind="lib" path="code/hppc-0.6.0.jar"/>
<classpathentry kind="output" path="bin"/>
</classpath>
......@@ -9,8 +9,8 @@ Require-Bundle: org.eclipse.core.runtime
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ClassPath: .,
code/grph-1.10.8.jar,
code/hppc-0.7.2.jar,
code/toools-0.1.8.jar
code/toools-0.1.8.jar,
code/hppc-0.6.0.jar
Export-Package: .,
com.carrotsearch.hppc,
com.carrotsearch.hppc.cursors,
......
......@@ -6,6 +6,6 @@ bin.includes = plugin.xml,\
.,\
src/,\
code/grph-1.10.8.jar,\
code/hppc-0.7.2.jar,\
code/toools-0.1.8.jar
code/toools-0.1.8.jar,\
code/hppc-0.6.0.jar
src.includes = code/
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