Browse Source
DdPrismModelBuilder now errors in case it has a program with unbounded integer variables as input
tempestpy_adaptions
Tim Quatmann
4 years ago
No known key found for this signature in database
GPG Key ID: 6EDE19592731EEC3
3 changed files with
21 additions and
1 deletions
resources/examples/testfiles/mdp/unbounded.nm
src/storm/builder/DdPrismModelBuilder.cpp
src/test/storm/builder/DdPrismModelBuilderTest.cpp
@ -0,0 +1,8 @@
mdp
const int N;
module main
x : int;
[] x<=0 -> (x'=x+1);
[] x>0 -> (x'=N*x);
endmodule
@ -541,7 +541,7 @@ namespace storm {
template < storm : : dd : : DdType Type , typename ValueType >
bool DdPrismModelBuilder < Type , ValueType > : : canHandle ( storm : : prism : : Program const & program ) {
return program . getModelType ( ) ! = storm : : prism : : Program : : ModelType : : PTA ;
return ! program . hasUnboundedVariables ( ) & & ( program . getModelType ( ) ! = storm : : prism : : Program : : ModelType : : PTA ) ;
}
template < storm : : dd : : DdType Type , typename ValueType >
@ -1311,6 +1311,7 @@ namespace storm {
stream < < " . " ;
STORM_LOG_THROW ( false , storm : : exceptions : : InvalidArgumentException , " Program still contains these undefined constants: " + stream . str ( ) ) ;
}
STORM_LOG_THROW ( ! program . hasUnboundedVariables ( ) , storm : : exceptions : : InvalidArgumentException , " Program contains unbounded variables which is not supported by the DD engine. " ) ;
STORM_LOG_TRACE ( " Building representation of program: " < < std : : endl < < program < < std : : endl ) ;
@ -319,3 +319,14 @@ TEST(DdPrismModelBuilderTest_Cudd, Composition) {
EXPECT_EQ ( 21ul , mdp - > getNumberOfChoices ( ) ) ;
}
TEST ( UnboundedTest_Sylvan , Mdp ) {
storm : : storage : : SymbolicModelDescription modelDescription = storm : : parser : : PrismParser : : parse ( STORM_TEST_RESOURCES_DIR " /mdp/unbounded.nm " ) ;
storm : : prism : : Program program = modelDescription . preprocess ( " N=1 " ) . asPrismProgram ( ) ;
EXPECT_FALSE ( storm : : builder : : DdPrismModelBuilder < storm : : dd : : DdType : : Sylvan > ( ) . canHandle ( program ) ) ;
}
TEST ( UnboundedTest_Cudd , Mdp ) {
storm : : storage : : SymbolicModelDescription modelDescription = storm : : parser : : PrismParser : : parse ( STORM_TEST_RESOURCES_DIR " /mdp/unbounded.nm " ) ;
storm : : prism : : Program program = modelDescription . preprocess ( " N=1 " ) . asPrismProgram ( ) ;
EXPECT_FALSE ( storm : : builder : : DdPrismModelBuilder < storm : : dd : : DdType : : CUDD > ( ) . canHandle ( program ) ) ;
}