artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Property selection

Browse Source
This commit is contained in:
Artur Meski
2018-07-17 20:26:05 +01:00
parent eb2e4e5526
commit b0d69d0aa7
3 changed files with 19 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
reactics.cc
View File

@@ -23,6 +23,7 @@ int main(int argc, char **argv)
bool benchmarking = false; bool benchmarking = false;
bool usage_error = false; bool usage_error = false;
bool print_parsed_sys = false; bool print_parsed_sys = false;
std::string property_name = "default";
static struct option long_options[] = { static struct option long_options[] = {
{"trace-parsing", no_argument, 0, 0 }, {"trace-parsing", no_argument, 0, 0 },
@@ -33,7 +34,7 @@ int main(int argc, char **argv)
int c; int c;
int option_index = 0; int option_index = 0;
while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxzh", long_options, while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzh", long_options,
&option_index)) != -1) { &option_index)) != -1) {
switch (c) { switch (c) {
case 0: case 0:
@@ -75,6 +76,7 @@ int main(int argc, char **argv)
case 'c': case 'c':
rstl_model_checking = true; rstl_model_checking = true;
property_name = optarg;
break; break;
case 'm': case 'm':
@@ -182,10 +184,10 @@ int main(int argc, char **argv)
if (rstl_model_checking) { if (rstl_model_checking) {
if (bmc) { if (bmc) {
cout << "Using BDD-based Bounded Model Checking" << endl; cout << "Using BDD-based Bounded Model Checking" << endl;
mc.checkRSCTLK(driver.getFormRSCTLK()); mc.checkRSCTLK(driver.getFormRSCTLK(property_name));
} }
else { else {
mc.checkRSCTLKfull(driver.getFormRSCTLK()); mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name));
} }
} }
} }

14
rsin_driver.cc
View File

@@ -17,7 +17,6 @@ rsin_driver::rsin_driver(RctSys *rs)
void rsin_driver::initialise(void) void rsin_driver::initialise(void)
{ {
rs = nullptr; rs = nullptr;
rsctlkform = nullptr;
opts = nullptr; opts = nullptr;
use_ctx_aut = false; use_ctx_aut = false;
use_concentrations = false; use_concentrations = false;
@@ -49,13 +48,18 @@ void rsin_driver::error(const std::string &m)
std::cerr << m << std::endl; std::cerr << m << std::endl;
} }
FormRSCTLK *rsin_driver::getFormRSCTLK(void) void rsin_driver::addFormRSCTLK(std::string propertyName, FormRSCTLK *f)
{ {
if (rsctlkform == nullptr) { properties[propertyName] = f;
FERROR("RSCTLK formula was not supplied!"); };
FormRSCTLK *rsin_driver::getFormRSCTLK(std::string propertyName)
{
if (properties.count(propertyName) == 0) {
FERROR("Property/formula label does not exist: " << propertyName);
} }
return rsctlkform; return properties[propertyName];
} }
// //

11
rsin_driver.hh
View File

@@ -25,9 +25,10 @@ class rsin_driver
virtual ~rsin_driver(); virtual ~rsin_driver();
//std::map<std::string, int> variables; //std::map<std::string, int> variables;
FormRSCTLK *rsctlkform;
Options *opts; Options *opts;
std::map<std::string, FormRSCTLK *> properties;
// options in configuration file: // options in configuration file:
bool use_ctx_aut; bool use_ctx_aut;
bool use_concentrations; bool use_concentrations;
@@ -45,11 +46,9 @@ class rsin_driver
{ {
this->opts = opts; this->opts = opts;
}; };
void addFormRSCTLK(std::string propertyName, FormRSCTLK *f) void addFormRSCTLK(std::string propertyName, FormRSCTLK *f);
{
rsctlkform = f; FormRSCTLK *getFormRSCTLK(std::string propertyName);
};
FormRSCTLK *getFormRSCTLK(void);
void ensureOptionsAllowed(void); void ensureOptionsAllowed(void);
void useContextAutomaton(void); void useContextAutomaton(void);