diff --git a/resources/examples/testfiles/ma/jobscheduler.ma b/resources/examples/testfiles/ma/jobscheduler.ma index 68f60fb55..152383eaf 100644 --- a/resources/examples/testfiles/ma/jobscheduler.ma +++ b/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; diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index 5f92999c1..fd29ceb67 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/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, "");