@ -92,40 +92,17 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
std : : string formulaAsString = " R>2.5 [F ((s=5) | (s=0&srep=3)) ] " ;
std : : string formulaAsString = " R>2.5 [F ((s=5) | (s=0&srep=3)) ] " ;
std : : string constantsAsString = " pL=0.9,TOAck=0.5 " ;
std : : string constantsAsString = " pL=0.9,TOAck=0.5 " ;
carl : : VariablePool : : getInstance ( ) . clear ( ) ;
carl : : VariablePool : : getInstance ( ) . clear ( ) ;
std : : cout < < " registred variables " < < std : : endl ;
carl : : printRegisteredVariableNames ( ) ;
std : : cout < < std : : endl ;
storm : : prism : : Program program = storm : : parseProgram ( programFile ) ;
storm : : prism : : Program program = storm : : parseProgram ( programFile ) ;
program = storm : : utility : : prism : : preprocess ( program , constantsAsString ) ;
program = storm : : utility : : prism : : preprocess ( program , constantsAsString ) ;
std : : cout < < " registred variables " < < std : : endl ;
carl : : printRegisteredVariableNames ( ) ;
std : : cout < < std : : endl ;
std : : vector < std : : shared_ptr < const storm : : logic : : Formula > > formulas = storm : : parseFormulasForProgram ( formulaAsString , program ) ; ;
std : : vector < std : : shared_ptr < const storm : : logic : : Formula > > formulas = storm : : parseFormulasForProgram ( formulaAsString , program ) ; ;
std : : shared_ptr < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > model = storm : : buildSparseModel < storm : : RationalFunction > ( program , formulas ) - > as < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > ( ) ;
std : : shared_ptr < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > model = storm : : buildSparseModel < storm : : RationalFunction > ( program , formulas ) - > as < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > ( ) ;
std : : cout < < " registred variables " < < std : : endl ;
carl : : printRegisteredVariableNames ( ) ;
std : : cout < < std : : endl ;
auto const & regionSettings = storm : : settings : : getModule < storm : : settings : : modules : : RegionSettings > ( ) ;
auto const & regionSettings = storm : : settings : : getModule < storm : : settings : : modules : : RegionSettings > ( ) ;
storm : : modelchecker : : region : : SparseRegionModelCheckerSettings settings ( regionSettings . getSampleMode ( ) , regionSettings . getApproxMode ( ) , regionSettings . getSmtMode ( ) ) ;
storm : : modelchecker : : region : : SparseRegionModelCheckerSettings settings ( regionSettings . getSampleMode ( ) , regionSettings . getApproxMode ( ) , regionSettings . getSmtMode ( ) ) ;
auto dtmcModelchecker = std : : make_shared < storm : : modelchecker : : region : : SparseDtmcRegionModelChecker < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > , double > > ( model , settings ) ;
auto dtmcModelchecker = std : : make_shared < storm : : modelchecker : : region : : SparseDtmcRegionModelChecker < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > , double > > ( model , settings ) ;
dtmcModelchecker - > specifyFormula ( formulas [ 0 ] ) ;
dtmcModelchecker - > specifyFormula ( formulas [ 0 ] ) ;
//start testing
//start testing
std : : cout < < " registred variables " < < std : : endl ;
carl : : printRegisteredVariableNames ( ) ;
std : : cout < < std : : endl ;
auto allSatRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.7<=pK<=0.875,0.75<=TOMsg<=0.95 " ) ;
auto allSatRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.7<=pK<=0.875,0.75<=TOMsg<=0.95 " ) ;
std : : cout < < " registred variables " < < std : : endl ;
carl : : printRegisteredVariableNames ( ) ;
std : : cout < < std : : endl ;
std : : cout < < " model parameters " < < std : : endl ;
for ( auto const & p : storm : : models : : sparse : : getProbabilityParameters ( * model ) ) {
std : : cout < < p . getId ( ) < < std : : endl ;
}
std : : cout < < " region parameters " < < std : : endl ;
for ( auto const & p : allSatRegion . getVariables ( ) ) {
std : : cout < < p . getId ( ) < < std : : endl ;
}
auto exBothRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.6<=pK<=0.9,0.5<=TOMsg<=0.95 " ) ;
auto exBothRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.6<=pK<=0.9,0.5<=TOMsg<=0.95 " ) ;
auto exBothHardRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.5<=pK<=0.75,0.3<=TOMsg<=0.4 " ) ; //this region has a local maximum!
auto exBothHardRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.5<=pK<=0.75,0.3<=TOMsg<=0.4 " ) ; //this region has a local maximum!
auto allVioRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.1<=pK<=0.3,0.2<=TOMsg<=0.3 " ) ;
auto allVioRegion = storm : : modelchecker : : region : : ParameterRegion < storm : : RationalFunction > : : parseRegion ( " 0.1<=pK<=0.3,0.2<=TOMsg<=0.3 " ) ;