Results
This commit is contained in:
16
reactics.cc
16
reactics.cc
@@ -158,6 +158,8 @@ int main(int argc, char **argv)
|
|||||||
//
|
//
|
||||||
auto rs = *driver.getReactionSystem();
|
auto rs = *driver.getReactionSystem();
|
||||||
|
|
||||||
|
bool result = true;
|
||||||
|
|
||||||
rs.setOptions(opts); // these need to be passed to the driver
|
rs.setOptions(opts); // these need to be passed to the driver
|
||||||
|
|
||||||
if (show_reactions) {
|
if (show_reactions) {
|
||||||
@@ -184,10 +186,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(property_name));
|
result = mc.checkRSCTLK(driver.getFormRSCTLK(property_name));
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name));
|
result = mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -213,7 +215,14 @@ int main(int argc, char **argv)
|
|||||||
|
|
||||||
delete opts;
|
delete opts;
|
||||||
|
|
||||||
return 0;
|
int ret_val;
|
||||||
|
|
||||||
|
if (result)
|
||||||
|
ret_val = 0;
|
||||||
|
else
|
||||||
|
ret_val = 1;
|
||||||
|
|
||||||
|
return ret_val;
|
||||||
}
|
}
|
||||||
|
|
||||||
void print_help(std::string path_str)
|
void print_help(std::string path_str)
|
||||||
@@ -258,4 +267,3 @@ void print_help(std::string path_str)
|
|||||||
}
|
}
|
||||||
|
|
||||||
/** EOF **/
|
/** EOF **/
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user