Skip to content

Commit e32cd3c

Browse files
folmatefolmate
committed
Storm analysis implementation (Environment, Interface, Codegen, SRV transformation)
1 parent 5e62406 commit e32cd3c

File tree

46 files changed

+1141
-1172
lines changed

Some content is hidden

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

46 files changed

+1141
-1172
lines changed

‎devenv/dockerfile‎

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,13 @@ EXPOSE 3389
99
# Initialize misc
1010
USER root
1111
RUN apt update
12-
RUN apt install git -y
13-
RUN apt install wget -y
12+
RUN apt install git wget zip nano -y
1413
RUN apt install openjdk-21-jdk -y
1514
RUN apt install psmisc -y
16-
RUN apt install nano -y
15+
RUN apt install webext-ublock-origin-firefox -y
1716
RUN apt install build-essential -y
1817

18+
1919
# Install ProbLog
2020
USER root
2121
RUN apt install -y python3
@@ -25,7 +25,7 @@ RUN pip install --break-system-packages PySDD
2525

2626
# Install eclipse
2727
USER root
28-
RUN wget 'https://www.eclipse.org/downloads/download.php?file=/technology/epp/downloads/release/2024-03/R/eclipse-modeling-2024-03-R-linux-gtk-x86_64.tar.gz&r=1' -O eclipse.tar.gz
28+
RUN wget 'https://www.eclipse.org/downloads/download.php?file=/technology/epp/downloads/release/2024-03/R/eclipse-modeling-2024-03-R-linux-gtk-x86_64.tar.gz' -O eclipse.tar.gz
2929
RUN tar -xzf eclipse.tar.gz -C /opt
3030
RUN rm eclipse.tar.gz
3131
RUN echo '[Desktop Entry]\n\
@@ -44,9 +44,22 @@ RUN /opt/eclipse/eclipse -application org.eclipse.equinox.p2.director -repositor
4444
RUN /opt/eclipse/eclipse -application org.eclipse.equinox.p2.director -repository http://download.eclipse.org/viatra/updates/release/2.8.0 -installIU org.eclipse.viatra.query.sdk.feature.source.feature.group/2.8.0.202310201322,org.eclipse.viatra.query.sdk.feature.feature.group/2.8.0.202310201322
4545

4646
# Install python packages for diagrams
47-
USER root
4847
RUN pip install --break-system-packages notebook
49-
RUN pip install --break-system-packages pandas==1.5.3 seaborn==0.12.2 matplotlib==3.7.1 numpy==1.26.4
48+
RUN pip install --break-system-packages pandas==1.5.3 seaborn==0.12.2 matplotlib==3.7.1 numpy==1.26.4 itables
5049

51-
RUN apt install webext-ublock-origin-firefox -y
52-
RUN rm -rf /config/.cache
50+
# Install storm
51+
USER root
52+
WORKDIR /opt
53+
RUN apt install build-essential git cmake libboost-all-dev libcln-dev libgmp-dev libginac-dev automake libglpk-dev libhwloc-dev libz3-dev libxerces-c-dev libeigen3-dev -y
54+
RUN wget https://github.com/moves-rwth/storm/archive/stable.zip
55+
RUN unzip stable.zip
56+
WORKDIR storm-stable
57+
RUN mkdir build
58+
WORKDIR build
59+
RUN cmake ..
60+
RUN make -j12
61+
ENV PATH=$PATH:/opt/storm-stable/build/bin
62+
WORKDIR /opt
63+
RUN rm stable.zip
64+
65+
RUN rm -rf /config/.cache

‎devenv/init.bat‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ cd /D "%~dp0"
55
docker run -d -u root ^
66
-v \\wsl$\Ubuntu\tmp\.X11-unix:/tmp/.X11-unix ^
77
-v \\wsl$\Ubuntu\mnt\wslg:/mnt/wslg ^
8-
--name=pgq-devenv ^
8+
--name=pgq-devenv-storm ^
99
--security-opt seccomp=unconfined ^
1010
-p 4100:3389 ^
1111
--shm-size="1gb" ^
1212
-v %~dp0\..:/config/ProbabilisticGraphQuery ^
13-
pgq-devenv
13+
pgq-devenv

‎devenv/workspace/se.liu.ida.sas.pelab.storm/.classpath‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<classpath>
3+
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17"/>
4+
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
5+
<classpathentry kind="src" path="src"/>
6+
<classpathentry kind="src" path="xtend-gen"/>
7+
<classpathentry kind="output" path="bin"/>
8+
</classpath>

‎devenv/workspace/se.liu.ida.sas.pelab.storm/.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/bin/

‎devenv/workspace/se.liu.ida.sas.pelab.storm/.project‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<projectDescription>
3+
<name>se.liu.ida.sas.pelab.storm</name>
4+
<comment></comment>
5+
<projects>
6+
</projects>
7+
<buildSpec>
8+
<buildCommand>
9+
<name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
10+
<arguments>
11+
</arguments>
12+
</buildCommand>
13+
<buildCommand>
14+
<name>org.eclipse.jdt.core.javabuilder</name>
15+
<arguments>
16+
</arguments>
17+
</buildCommand>
18+
<buildCommand>
19+
<name>org.eclipse.pde.ManifestBuilder</name>
20+
<arguments>
21+
</arguments>
22+
</buildCommand>
23+
<buildCommand>
24+
<name>org.eclipse.pde.SchemaBuilder</name>
25+
<arguments>
26+
</arguments>
27+
</buildCommand>
28+
</buildSpec>
29+
<natures>
30+
<nature>org.eclipse.pde.PluginNature</nature>
31+
<nature>org.eclipse.jdt.core.javanature</nature>
32+
<nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
33+
</natures>
34+
</projectDescription>

‎devenv/workspace/se.liu.ida.sas.pelab.storm/.settings/org.eclipse.core.resources.prefs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
eclipse.preferences.version=1
2+
encoding/<project>=UTF-8

‎devenv/workspace/se.liu.ida.sas.pelab.storm/.settings/org.eclipse.jdt.core.prefs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
eclipse.preferences.version=1
2+
org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
3+
org.eclipse.jdt.core.compiler.compliance=17
4+
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
5+
org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
6+
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
7+
org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
8+
org.eclipse.jdt.core.compiler.release=enabled
9+
org.eclipse.jdt.core.compiler.source=17

‎devenv/workspace/se.liu.ida.sas.pelab.storm/META-INF/MANIFEST.MF‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
Manifest-Version: 1.0
2+
Bundle-ManifestVersion: 2
3+
Bundle-Name: Storm
4+
Bundle-SymbolicName: se.liu.ida.sas.pelab.storm
5+
Bundle-Version: 1.0.0.qualifier
6+
Export-Package: se.liu.ida.sas.pelab.storm.run,
7+
se.liu.ida.sas.pelab.storm.transformation
8+
Automatic-Module-Name: se.liu.ida.sas.pelab.storm
9+
Bundle-RequiredExecutionEnvironment: JavaSE-17
10+
Require-Bundle: com.google.guava,
11+
org.eclipse.xtext.xbase.lib,
12+
org.eclipse.xtend.lib,
13+
org.eclipse.xtend.lib.macro,
14+
hu.bme.mit.inf.measurement.utilities;bundle-version="1.0.0"

‎devenv/workspace/se.liu.ida.sas.pelab.storm/build.properties‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
source.. = src/
2+
output.. = bin/
3+
bin.includes = META-INF/,\
4+
.

‎devenv/workspace/se.liu.ida.sas.pelab.storm/src/se/liu/ida/sas/pelab/storm/run/StormEvaluation.xtend‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
package se.liu.ida.sas.pelab.storm.run
2+
3+
import hu.bme.mit.inf.measurement.utilities.Config
4+
import java.util.regex.Pattern
5+
import java.util.HashMap
6+
import java.util.Scanner
7+
import java.io.File
8+
import java.io.FileWriter
9+
import hu.bme.mit.inf.measurement.utilities.configuration.BaseConfiguration
10+
import java.io.BufferedReader
11+
import java.util.Map
12+
import org.eclipse.xtext.xbase.lib.Functions.Function0
13+
import java.util.List
14+
15+
class StormEvaluation {
16+
static val Pattern pattern = Pattern.compile("^System failure probability at timebound 1 is ([01]\\.\\d*)$")
17+
18+
static def evalueate(BaseConfiguration cfg, Function0<Pair<String,List<String>>> generator) {
19+
var results = newHashMap
20+
var cumTransformationTime = 0.0
21+
var cumAnalysisTime = 0.0
22+
23+
/**
24+
* Transform base model
25+
* (measured as transformation)
26+
*/
27+
val start = System.nanoTime
28+
val value = generator.apply()
29+
val end = System.nanoTime
30+
val basemodel = value.key
31+
val tops = value.value
32+
cumTransformationTime += (end - start) / 1000.0 / 1000.0 // convert nano seconds to ms
33+
34+
for (top : tops) {
35+
//`println('''TOP: «top»''')
36+
var remainingtime_ms = (cfg.timeoutS * 1000) - (cumAnalysisTime + cumTransformationTime)
37+
if (remainingtime_ms > 0) {
38+
val time = Math.round(Math.ceil(remainingtime_ms / 1000.0))
39+
40+
/**
41+
* Setup analysis model
42+
* (measured as transformation)
43+
*/
44+
val trafoStart = System.nanoTime
45+
val file = new File(cfg.stormFile)
46+
println(file.absolutePath)
47+
file.createNewFile
48+
val writer = new FileWriter(file)
49+
writer.write('''
50+
«top»
51+
«basemodel»
52+
''')
53+
writer.flush
54+
writer.close()
55+
val trafoEnd = System.nanoTime
56+
/**
57+
* Run analysis
58+
* (measured as analysis)
59+
*/
60+
val analysisStart = System.nanoTime
61+
val builder = new ProcessBuilder("storm-dft", "-dft", cfg.stormFile,
62+
"--timebound", "1",
63+
"--bdd",
64+
"--precision", "1e-09",
65+
"--timeout", time.toString);
66+
val process = builder.start
67+
/**
68+
* Process results
69+
*/
70+
val io = new Scanner(process.inputStream)
71+
while (io.hasNextLine) {
72+
val line = io.nextLine
73+
println('''DEBUG: «line»''')
74+
val match = pattern.matcher(line)
75+
if (match.find) {
76+
results.put(top, Double.parseDouble(match.group(1)))
77+
}
78+
}
79+
val analysisEnd = System.nanoTime
80+
/**
81+
* Update configuration
82+
*/
83+
cumAnalysisTime += (analysisEnd - analysisStart) / 1000.0 / 1000.0 // convert nano seconds to ms
84+
cumTransformationTime += (trafoEnd - trafoStart) / 1000.0 / 1000.0 // convert nano seconds to ms
85+
}
86+
}
87+
var remainingtime_ms = (cfg.timeoutS * 1000) - (cumAnalysisTime + cumTransformationTime)
88+
val timeout = remainingtime_ms < 0
89+
return new StormRunInfo(cumTransformationTime, cumAnalysisTime, results, timeout)
90+
}
91+
}
92+
93+
class StormRunInfo {
94+
public val double transformation_ms
95+
public val double run_ms
96+
public val Map<String, Double> results
97+
public val boolean timeout
98+
99+
new(double trafo, double run, Map<String, Double> results, boolean timeout) {
100+
this.transformation_ms = trafo
101+
this.run_ms = run
102+
this.results = results
103+
this.timeout = timeout
104+
}
105+
}

0 commit comments

Comments
 (0)