Skip to content

Commit 8aa5706

Browse files
KiguliKiguli
committed
ARCH-COMP25 benchmarks
1 parent 6b314fa commit 8aa5706

File tree

18 files changed

+1207
-0
lines changed

18 files changed

+1207
-0
lines changed

‎examples/ARCH-COMP/2025/AS/AS.cpp‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
// Run: make
2+
// Then: ./AS
3+
4+
// Code: Ben Wooding 8 Apr 2025
5+
6+
#include <iostream>
7+
#include <vector>
8+
#include <functional>
9+
#include "../../../../src/IMDP.h"
10+
#include <armadillo>
11+
#include <chrono>
12+
13+
using namespace std;
14+
using namespace arma;
15+
16+
/*
17+
################################# PARAMETERS ###############################################
18+
*/
19+
20+
// Set the dimensions
21+
const int dim_x = 3;
22+
const int dim_u = 2;
23+
const int dim_w = 0;
24+
25+
// Define lower bounds, upper bounds, and step sizes
26+
// States
27+
const vec ss_lb = {1,0, 0};
28+
const vec ss_ub = {6,10, 10};
29+
const vec ss_eta = {0.25,1,1};
30+
// Inputs
31+
const vec is_lb = {0,0};
32+
const vec is_ub = {7,30};
33+
const vec is_eta = {1,30};
34+
35+
//standard deviation of each dimension
36+
const vec sigma = {sqrt(0.001), sqrt(0.001), sqrt(0.001)};
37+
38+
// logical expression for target region
39+
auto target_condition = [](const vec& ss) { return (ss[0] >= 4.0 && ss[0] <= 6.0) && (ss[1] >= 8.0 && ss[1] <= 10.0) && (ss[2] >= 8.0 && ss[2] <= 10.0); };
40+
41+
//dynamics - 3 parameters
42+
auto dynamics = [](const vec& x, const vec& u) -> vec {
43+
vec xx(dim_x);
44+
xx[0] = 0.8192*x[0] + 0.03412*x[1] +0.01265*x[2] + 0.01883*(u[0] + u[1]);
45+
xx[1] = 0.01646*x[0] + 0.9822*x[1] +0.0001*x[2] + 0.0002*(u[0] + u[1]);
46+
xx[2] = 0.0009*x[0] + 0.00002*x[1] +0.9989*x[2] + 0.00001*(u[0] + u[1]);
47+
return xx;
48+
};
49+
50+
/*
51+
################################# MAIN FUNCTION ##############################################
52+
*/
53+
54+
int main() {
55+
56+
/* ###### create IMDP object ###### */
57+
IMDP mdp(dim_x,dim_u,dim_w);
58+
59+
/* ###### create finite sets for the different spaces ###### */
60+
mdp.setStateSpace(ss_lb, ss_ub, ss_eta);
61+
mdp.setInputSpace(is_lb, is_ub, is_eta);
62+
//mdp.setDisturbSpace(ws_lb, ws_ub, ws_eta);
63+
64+
/* ###### relabel states based on specification ###### */
65+
mdp.setTargetSpace(target_condition, true);
66+
67+
/*###### save the files ######*/
68+
//mdp.saveStateSpace();
69+
//mdp.saveInputSpace();
70+
//mdp.saveDisturbSpace();
71+
//mdp.saveTargetSpace();
72+
73+
/*###### set dynamics and noise ######*/
74+
mdp.setDynamics(dynamics);
75+
mdp.setNoise(NoiseType::NORMAL);
76+
mdp.setStdDev(sigma);
77+
78+
/* ###### calculate abstraction for target vectors ######*/
79+
/// each bound can be done seperately using:
80+
//mdp.minTargetTransitionVector();
81+
//mdp.maxTargetTransitionVector();
82+
///or combined using:
83+
mdp.targetTransitionVectorBounds();
84+
85+
/* ###### save target vectors ######*/
86+
//mdp.saveMinTargetTransitionVector();
87+
//mdp.saveMaxTargetTransitionVector();
88+
89+
/* ###### calculate abstraction for avoid vectors ######*/
90+
mdp.minAvoidTransitionVector();
91+
mdp.maxAvoidTransitionVector();
92+
93+
/* ###### save avoid vectors ######*/
94+
//mdp.saveMinAvoidTransitionVector();
95+
//mdp.saveMaxAvoidTransitionVector();
96+
97+
/* ###### calculate abstraction for transition matrices ######*/
98+
/// each bound can be done seperately using:
99+
//mdp.minTransitionMatrix();
100+
//mdp.maxTransitionMatrix();
101+
///or combined using:
102+
mdp.transitionMatrixBounds();
103+
104+
/* ###### save transition matrices ######*/
105+
//mdp.saveMinTransitionMatrix();
106+
//mdp.saveMaxTransitionMatrix();
107+
108+
/* ###### synthesize infinite horizon controller (true = pessimistic, false = optimistic) ######*/
109+
//mdp.infiniteHorizonReachControllerSorted(true);
110+
111+
/* ###### synthesize finite horizon controller (true = pessimistic, false = optimistic) ######*/
112+
mdp.finiteHorizonReachControllerSorted(true,10);
113+
114+
/* ###### save controller ######*/
115+
mdp.saveController();
116+
117+
return 0;
118+
}

‎examples/ARCH-COMP/2025/AS/Makefile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CC = acpp # or syclcc (then remove --acpp-targets="omp")
2+
ARCH := $(shell uname -m)
3+
CFLAGS = --acpp-targets="omp" -O3 -lnlopt -lm -I/usr/include/hdf5/serial -L/usr/lib/$(ARCH)-linux-gnu/hdf5/serial -lhdf5 -lglpk -lgsl -lgslcblas -DH5_USE_110_API -larmadillo
4+
5+
# Find all .cpp files in the current directory
6+
CPP_FILES := $(wildcard *.cpp)
7+
8+
# Generate corresponding executable names
9+
EXECUTABLES := $(patsubst %.cpp,%,$(CPP_FILES))
10+
11+
all: $(EXECUTABLES)
12+
13+
%: %.cpp ../../../../src/IMDP.cpp ../../../../src/MDP.cpp
14+
$(CC) $^ $(CFLAGS) -o $@
15+
16+
clean:
17+
rm -f $(EXECUTABLES)
18+

‎examples/ARCH-COMP/2025/AV_minimal/AV_minimal.cpp‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
// Run: make
2+
// ./vehicle3D
3+
4+
// Code: Ben Wooding 6 Jan 2024
5+
6+
#include <iostream>
7+
#include <vector>
8+
#include <functional>
9+
#include "../../../../src/IMDP.h"
10+
#include <chrono>
11+
#include <armadillo>
12+
13+
using namespace std;
14+
using namespace arma;
15+
16+
/*
17+
################################# PARAMETERS ###############################################
18+
*/
19+
20+
// Set the dimensions
21+
const int dim_x = 3;
22+
const int dim_u = 2;
23+
const int dim_w = 0;
24+
25+
// Define lower bounds, upper bounds, and step sizes
26+
// States
27+
const vec ss_lb = {-5.0, -5.0,-3.4};
28+
const vec ss_ub = {5.0, 5.0, 3.4};
29+
const vec ss_eta = {0.5, 0.5,0.4};
30+
// Inputs
31+
const vec is_lb = {-1.0,-0.4};
32+
const vec is_ub = {4.0,0.4};
33+
const vec is_eta = {1, 0.2};
34+
35+
//standard deviation of each dimension
36+
const vec sigma = {sqrt(1/1.5), sqrt(1/1.5),sqrt(1/1.5)};
37+
38+
// logical expression for target region and avoid region
39+
auto target_condition = [](const vec& ss) { return (ss(0) >= -5.75 && ss(0) <= 0.25) && (ss(1) >= -0.25 && ss(1) <= 5.75) && (ss(2) >= -3.45 && ss(2) <= 3.45);};
40+
auto avoid_condition = [](const vec& ss) { return (ss(0) >= -5.75 && ss(0) <= 0.25) && (ss(1) >= -0.75 && ss(1) <= -0.25) && (ss(2) >= -3.45 && ss(2) <= 3.45);};
41+
42+
//dynamics - 2 parameters
43+
const auto dynamics = [](const vec& x, const vec& u) -> vec {
44+
float Ts = 0.100;
45+
vec f(3);
46+
vec xx = x;
47+
48+
f[0] = u[0]*cos(atan((float)(tan(u[1])/2.0))+xx[2])/cos((float)atan((float)(tan(u[1])/2.0)));
49+
f[1] = u[0]*sin(atan((float)(tan(u[1])/2.0))+xx[2])/cos((float)atan((float)(tan(u[1])/2.0)));
50+
f[2] = u[0]*tan(u[1]);
51+
52+
xx = xx + Ts*f;
53+
return xx;
54+
};
55+
56+
/*
57+
################################# MAIN FUNCTION ######################################
58+
*/
59+
60+
int main() {
61+
62+
/* ###### create IMDP object ###### */
63+
IMDP mdp(dim_x,dim_u,dim_w);
64+
65+
/* ###### create finite sets for the different spaces ###### */
66+
mdp.setStateSpace(ss_lb, ss_ub, ss_eta);
67+
mdp.setInputSpace(is_lb, is_ub, is_eta);
68+
69+
/* ###### relabel states based on specification ###### */
70+
mdp.setTargetAvoidSpace(target_condition,avoid_condition, true);
71+
72+
/*###### save the files ######*/
73+
//mdp.saveStateSpace();
74+
//mdp.saveInputSpace();
75+
//mdp.saveTargetSpace();
76+
77+
/*###### set dynamics and noise ######*/
78+
mdp.setDynamics(dynamics);
79+
mdp.setNoise(NoiseType::NORMAL);
80+
mdp.setStdDev(sigma);
81+
82+
/* ###### calculate abstraction for target vectors ######*/
83+
mdp.targetTransitionVectorBounds();
84+
85+
/* ###### save target vectors ######*/
86+
//mdp.saveMinTargetTransitionVector();
87+
//mdp.saveMaxTargetTransitionVector();
88+
89+
/* ###### calculate abstraction for avoid vectors ######*/
90+
mdp.minAvoidTransitionVector();
91+
mdp.maxAvoidTransitionVector();
92+
93+
/* ###### save avoid vectors ######*/
94+
//mdp.saveMinAvoidTransitionVector();
95+
//mdp.saveMaxAvoidTransitionVector();
96+
97+
98+
/* ###### calculate abstraction for transition matrices ######*/
99+
mdp.transitionMatrixBounds();
100+
101+
/* ###### save transition matrices ######*/
102+
//mdp.saveMinTransitionMatrix();
103+
//mdp.saveMaxTransitionMatrix();
104+
105+
/* ###### synthesize infinite horizon controller (true = pessimistic, false = optimistic) ######*/
106+
mdp.infiniteHorizonReachControllerSorted(true);
107+
108+
/* ###### synthesize finite horizon controller (true = pessimistic, false = optimistic) ######*/
109+
//mdp.finiteHorizonReachControllerSorted(true,10);
110+
111+
/* ###### save controller ######*/
112+
//mdp.saveController();
113+
114+
return 0;
115+
}

‎examples/ARCH-COMP/2025/AV_minimal/Makefile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CC = acpp # or syclcc (then remove --acpp-targets="omp")
2+
ARCH := $(shell uname -m)
3+
CFLAGS = --acpp-targets="omp" -O3 -lnlopt -lm -I/usr/include/hdf5/serial -L/usr/lib/$(ARCH)-linux-gnu/hdf5/serial -lhdf5 -lglpk -lgsl -lgslcblas -DH5_USE_110_API -larmadillo
4+
5+
# Find all .cpp files in the current directory
6+
CPP_FILES := $(wildcard *.cpp)
7+
8+
# Generate corresponding executable names
9+
EXECUTABLES := $(patsubst %.cpp,%,$(CPP_FILES))
10+
11+
all: $(EXECUTABLES)
12+
13+
%: %.cpp ../../../../src/IMDP.cpp ../../../../src/MDP.cpp
14+
$(CC) $^ $(CFLAGS) -o $@
15+
16+
clean:
17+
rm -f $(EXECUTABLES)
18+

‎examples/ARCH-COMP/2025/BA/BA_4d.cpp‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
// Run: make
2+
// ./BAS4D
3+
4+
// Created by Ben Wooding 6 Jan 2024
5+
6+
#include <iostream>
7+
#include <vector>
8+
#include <functional>
9+
#include "../../../../src/IMDP.h"
10+
#include <armadillo>
11+
#include <chrono>
12+
13+
using namespace arma;
14+
using namespace std;
15+
16+
/*
17+
################################# PARAMETERS ###############################################
18+
*/
19+
20+
// Set the dimensions
21+
const int dim_x = 4;
22+
const int dim_u = 1;
23+
const int dim_w = 0;
24+
25+
// Define lower bounds, upper bounds, and step sizes
26+
// States
27+
const vec ss_lb = {19.0, 19.0, 30.0, 30.0};
28+
const vec ss_ub = {21.0, 21.0, 36.0, 36.0};
29+
const vec ss_eta = {0.5, 0.5, 1.0, 1.0};
30+
// Inputs
31+
const vec is_lb = {17.0};
32+
const vec is_ub = {20.0};
33+
const vec is_eta = {1.0};
34+
35+
//standard deviation of each dimension
36+
const vec sigma = {sqrt(0.0774), sqrt(0.0774),sqrt(0.3872), sqrt(0.3098)};
37+
38+
//dynamics - 2 parameters
39+
auto dynamics = [](const vec& x, const vec& u) -> vec {
40+
vec xx(dim_x);
41+
const mat A = {{0.6682, 0.0, 0.02632, 0.0}, {0.0, 0.6830, 0.0, 0.02096}, {1.0005, 0.0, -0.000499, 0.0}, {0.0, 0.8004, 0.0, 0.1996}};
42+
const vec B = {0.1320, 0.1402, 0.0, 0.0};
43+
const vec Q = {3.4378, 2.9272, 13.0207, 10.4166};
44+
45+
xx = A*x + B*u + Q;
46+
return xx;
47+
};
48+
49+
/*
50+
################################# MAIN FUNCTION ##############################################
51+
*/
52+
53+
int main() {
54+
55+
/* ###### create IMDP object ###### */
56+
IMDP mdp(dim_x,dim_u,dim_w);
57+
58+
/* ###### create finite sets for the different spaces ###### */
59+
mdp.setStateSpace(ss_lb, ss_ub, ss_eta);
60+
mdp.setInputSpace(is_lb, is_ub, is_eta);
61+
62+
/*###### save the files ######*/
63+
//mdp.saveStateSpace();
64+
//mdp.saveInputSpace();
65+
66+
/*###### set dynamics and noise ######*/
67+
mdp.setDynamics(dynamics);
68+
mdp.setNoise(NoiseType::NORMAL);
69+
mdp.setStdDev(sigma);
70+
71+
/* ###### calculate abstraction for avoid vectors ######*/
72+
mdp.minAvoidTransitionVector();
73+
mdp.maxAvoidTransitionVector();
74+
75+
/* ###### save avoid vectors ######*/
76+
//mdp.saveMinAvoidTransitionVector();
77+
//mdp.saveMaxAvoidTransitionVector();
78+
79+
/* ###### calculate abstraction for transition matrices ######*/
80+
mdp.transitionMatrixBounds();
81+
82+
/* ###### save transition matrices ######*/
83+
//mdp.saveMinTransitionMatrix();
84+
//mdp.saveMaxTransitionMatrix();
85+
86+
/* ###### synthesize infinite horizon controller (true = pessimistic, false = optimistic) ######*/
87+
//mdp.infiniteHorizonSafeControllerSorted(true);
88+
89+
/* ###### synthesize finite horizon controller (true = pessimistic, false = optimistic) ######*/
90+
mdp.finiteHorizonSafeControllerSorted(true,6);
91+
92+
/* ###### save controller ######*/
93+
mdp.saveController();
94+
95+
return 0;
96+
}
97+
98+

‎examples/ARCH-COMP/2025/BA/Makefile‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CC = acpp # or syclcc (then remove --acpp-targets="omp")
2+
ARCH := $(shell uname -m)
3+
CFLAGS = --acpp-targets="omp" -O3 -lnlopt -lm -I/usr/include/hdf5/serial -L/usr/lib/$(ARCH)-linux-gnu/hdf5/serial -lhdf5 -lglpk -lgsl -lgslcblas -DH5_USE_110_API -larmadillo
4+
5+
# Find all .cpp files in the current directory
6+
CPP_FILES := $(wildcard *.cpp)
7+
8+
# Generate corresponding executable names
9+
EXECUTABLES := $(patsubst %.cpp,%,$(CPP_FILES))
10+
11+
all: $(EXECUTABLES)
12+
13+
%: %.cpp ../../../../src/IMDP.cpp ../../../../src/MDP.cpp
14+
$(CC) $^ $(CFLAGS) -o $@
15+
16+
clean:
17+
rm -f $(EXECUTABLES)
18+

0 commit comments

Comments
 (0)