Browse Source

.... actually fixed pcaa tests

tempestpy_adaptions
TimQu 8 years ago
parent
commit
18dac3231e
  1. 1
      resources/examples/testfiles/ma/jobscheduler.ma
  2. 2
      src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp

1
resources/examples/testfiles/ma/jobscheduler.ma

@ -37,6 +37,7 @@ init
endinit
label "all_jobs_finished" = num_finished=3;
label "half_of_jobs_finished" = num_finished=2;
label "one_job_finished" = num_finished=1;
label "slowest_before_fastest" = f_j1=1 & f_j3=0;
rewards "avg_waiting_time"
true : (3-num_finished)/3;

2
src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp

@ -155,7 +155,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) {
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 \"all_jobs_finished\"]) ";
std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) ";
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");

Loading…
Cancel
Save