-
Notifications
You must be signed in to change notification settings - Fork 3
/
config.properties
118 lines (88 loc) · 3.34 KB
/
config.properties
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
#Note: Automatic transformation of QoS requirements to constraints and minimisation/maximisation objectives
# is currently under development. For the time being, the user should define the constraints & objectives
# within the appropriate properties (e.g., pctl, csl) file.
#Step 1:Set the probabilistic model template and the probabilistic temporal logic formulae files of the problem
PROBLEM = MARC
#FX
# MODEL_TEMPLATE_FILE = models/FX/fxSmall.pm
# PROPERTIES_FILE = models/FX/fxSmall.pctl
#DPM
# MODEL_TEMPLATE_FILE = models/DPMParam/dpmSmall.pm
# PROPERTIES_FILE = models/DPMParam/dpmSmall.csl
#Zeroconf
#MODEL_TEMPLATE_FILE = models/Zeroconf/zeroconf.pm
#PROPERTIES_FILE = models/Zeroconf/zeroconf.pctl
#COPE
# MODEL_TEMPLATE_FILE = models/COPE/copeModel.pm
# PROPERTIES_FILE = models/cope/copeProperties.pctl
#DIE
# MODEL_TEMPLATE_FILE = models/dieParam/die.pm
# PROPERTIES_FILE = models/dieParam/die.pctl
#ePMC
# MODEL_TEMPLATE_FILE = models/ePMC/epmc.pm
# PROPERTIES_FILE = models/ePMC/epmc.pctl
#Virus
# MODEL_TEMPLATE_FILE = models/VirusHAIQ/virus-evolvableparameter.pm
# PROPERTIES_FILE = models/VirusHAIQ/virus.pctl
#Google
# MODEL_TEMPLATE_FILE = models/Google/googleTemplate.sm
# PROPERTIES_FILE = models/Google/google.csl
#Cobot
# MODEL_TEMPLATE_FILE = models/Cobot/teconnex07.pm
# PROPERTIES_FILE = models/Cobot/teconnex05.pctl
#Gricel
# MODEL_TEMPLATE_FILE = models/Gricel/robotsv1.pm
# PROPERTIES_FILE = models/Gricel/robotsv1.pctl
#Marc
MODEL_TEMPLATE_FILE = models/MarcRobot/model_10.prism
PROPERTIES_FILE = models/MarcRobot/model_10.pctl
#PAL
# MODEL_TEMPLATE_FILE = models/SESAME-EDDI/palEvoChecker.prism
# PROPERTIES_FILE = models/SESAME-EDDI/pal.csl
# MODEL_TEMPLATE_FILE = models/SESAME-EDDI/pal_dtmc.prism
# PROPERTIES_FILE = models/SESAME-EDDI/pal_dtmc.props
#Step2 : Set the algorithm (MOGA or Random) to run
#ALGORITHM = RANDOM
ALGORITHM = NSGAII
#ALGORITHM = SPEA2
#ALGORITHM = MOCELL
#Step 3: Set the population for the MOGAs
POPULATION_SIZE = 40
#Step 4: Set the maximum number of evaluations
MAX_EVALUATIONS = 200
#Step 5: Set the number of processors (for parallel execution) and initial port
PROCESSORS = 1
INIT_PORT = 8860
#Step 6: Set the directories containing the libraries of the model checker
MODEL_CHECKING_ENGINE_LIBS_DIRECTORY = libs/runtime-amd64
#Step 7: Set plotting settings
#Note: requires Python3
PLOT_PARETO_FRONT = TRUE
PYTHON3_DIRECTORY = /usr/bin/python3
# /usr/local/bin/python3
#Step 8: Set additional settings
VERBOSE = TRUE
#Which EvoChecker engine should be used: Options: NORMAL, PARAMETRIC
#If is absent the normal EvoChecker will be used
#EVOCHECKER_TYPE = NORMAL
#Option: PRISM | STORM (preference: PRISM for NORMAL, STORM for PARAMETRIC)
# EVOCHECKER_ENGINE = PRISM
# EVOCHECKER_TYPE = PARAMETRIC
# EVOCHECKER_ENGINE = STORM
EVOCHECKER_TYPE = NORMAL
EVOCHECKER_ENGINE = PRISM
#Step 9: Run
# Within your main class do:
# 1) Create EvoChecker instance
# EvoChecker ec = new EvoChecker();
#
# 2) Set configuration file
# String configFile ="resources/config.properties";
# ec.setConfigurationFile(configFile);
#
# 3) Start EvoChecker
# ec.start();
#############################################################3
#Advanced Settings
# JAVA=/Library/Java/JavaVirtualMachines/openjdk-11.0.2.jdk/Contents/Home/bin/java
# MODEL_CHECKING_ENGINE = libs/PrismExecutor.jar