@ -1,259 +1,52 @@
# include "storm/cli/cli.h"
# pragma once
# include "storm/api/storm.h"
# include "storm/utility/resources.h"
# include "storm/utility/file.h"
# include "storm/utility/storm-version.h"
# include "storm/utility/macros.h"
# include "storm/utility/initialize.h"
# include "storm/utility/Stopwatch.h"
# include <type_traits>
# include <chrono>
# include <ctime>
# include <sstream>
# include <iomanip>
# include "storm/storage/SymbolicModelDescription.h"
# include "storm/models/ModelBase.h"
# include "storm/settings/modules/DebugSettings.h"
# include "storm/settings/modules/IOSettings.h"
# include "storm/settings/modules/CoreSettings.h"
# include "storm/exceptions/OptionParserException.h"
# include "storm/settings/modules/ResourceSettings.h"
# include "storm/settings/modules/JaniExportSettings.h"
# include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
# include "storm/models/sparse/StandardRewardModel.h"
# include "storm/models/symbolic/StandardRewardModel.h"
# include "storm/utility/resources.h"
# include "storm/utility/file.h"
# include "storm/utility/storm-version.h"
# include "storm/utility/cli.h"
# include "storm/utility/initialize.h"
# include "storm/utility/Stopwatch.h"
# include "storm/settings/SettingsManager.h"
# include "storm/settings/modules/ResourceSettings.h"
# include "storm/settings/modules/JitBuilderSettings.h"
# include "storm/settings/modules/DebugSettings.h"
# include "storm/settings/modules/IOSettings.h"
# include "storm/settings/modules/CoreSettings.h"
# include "storm/settings/modules/ResourceSettings.h"
# include "storm/settings/modules/JaniExportSettings.h"
# include <type_traits>
# include "storm/api/storm.h"
# include "storm/utility/macros.h"
/ / Includes for the linked libraries and versions header .
# ifdef STORM_HAVE_INTELTBB
# include "tbb / tbb_stddef.h"
# endif
# ifdef STORM_HAVE_GLPK
# include "glpk.h"
# endif
# ifdef STORM_HAVE_GUROBI
# include "gurobi_c.h"
# endif
# ifdef STORM_HAVE_Z3
# include "z3.h"
# endif
# ifdef STORM_HAVE_MSAT
# include "mathsat.h"
# endif
# ifdef STORM_HAVE_CUDA
# include <cuda.h>
# include <cuda_runtime.h>
# endif
# ifdef STORM_HAVE_SMTRAT
# include "lib/smtrat.h"
# endif
# include "storm/utility/Stopwatch.h"
namespace storm {
namespace cli {
int64_t process ( const int argc , const char * * argv ) {
storm : : utility : : setUp ( ) ;
storm : : cli : : printHeader ( " Storm " , argc , argv ) ;
storm : : settings : : initializeAll ( " Storm " , " storm " ) ;
storm : : utility : : Stopwatch totalTimer ( true ) ;
if ( ! storm : : cli : : parseOptions ( argc , argv ) ) {
return - 1 ;
}
processOptions ( ) ;
totalTimer . stop ( ) ;
if ( storm : : settings : : getModule < storm : : settings : : modules : : ResourceSettings > ( ) . isPrintTimeAndMemorySet ( ) ) {
storm : : cli : : printTimeAndMemoryStatistics ( totalTimer . getTimeInMilliseconds ( ) ) ;
}
storm : : utility : : cleanUp ( ) ;
return 0 ;
}
std : : string currentTimeAndDate ( ) {
auto now = std : : chrono : : system_clock : : now ( ) ;
auto in_time_t = std : : chrono : : system_clock : : to_time_t ( now ) ;
std : : stringstream ss ;
ss < < std : : put_time ( std : : localtime ( & in_time_t ) , " %d/%m/%Y %X " ) ;
return ss . str ( ) ;
}
void printHeader ( std : : string const & name , const int argc , const char * argv [ ] ) {
STORM_PRINT ( name < < " " < < storm : : utility : : StormVersion : : shortVersionString ( ) < < std : : endl < < std : : endl ) ;
/ / " Compute " the command line argument string with which storm was invoked .
std : : stringstream commandStream ;
for ( int i = 1 ; i < argc ; + + i ) {
commandStream < < argv [ i ] < < " " ;
}
std : : string command = commandStream . str ( ) ;
if ( ! command . empty ( ) ) {
STORM_PRINT ( " Command line arguments: " < < commandStream . str ( ) < < std : : endl ) ;
STORM_PRINT ( " Current working directory: " < < storm : : utility : : cli : : getCurrentWorkingDirectory ( ) < < std : : endl ) ;
STORM_PRINT ( " Current date/time: " < < currentTimeAndDate ( ) < < std : : endl < < std : : endl ) ;
}
}
void printVersion ( std : : string const & name ) {
STORM_PRINT ( storm : : utility : : StormVersion : : longVersionString ( ) < < std : : endl ) ;
STORM_PRINT ( storm : : utility : : StormVersion : : buildInfo ( ) < < std : : endl ) ;
# ifdef STORM_HAVE_INTELTBB
STORM_PRINT ( " Linked with Intel Threading Building Blocks v " < < TBB_VERSION_MAJOR < < " . " < < TBB_VERSION_MINOR < < " (Interface version " < < TBB_INTERFACE_VERSION < < " ). " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_GLPK
STORM_PRINT ( " Linked with GNU Linear Programming Kit v " < < GLP_MAJOR_VERSION < < " . " < < GLP_MINOR_VERSION < < " . " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_GUROBI
STORM_PRINT ( " Linked with Gurobi Optimizer v " < < GRB_VERSION_MAJOR < < " . " < < GRB_VERSION_MINOR < < " . " < < GRB_VERSION_TECHNICAL < < " . " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_Z3
unsigned int z3Major , z3Minor , z3BuildNumber , z3RevisionNumber ;
Z3_get_version ( & z3Major , & z3Minor , & z3BuildNumber , & z3RevisionNumber ) ;
STORM_PRINT ( " Linked with Microsoft Z3 Optimizer v " < < z3Major < < " . " < < z3Minor < < " Build " < < z3BuildNumber < < " Rev " < < z3RevisionNumber < < " . " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_MSAT
char * msatVersion = msat_get_version ( ) ;
STORM_PRINT ( " Linked with " < < msatVersion < < " . " < < std : : endl ) ;
msat_free ( msatVersion ) ;
# endif
# ifdef STORM_HAVE_SMTRAT
STORM_PRINT ( " Linked with SMT-RAT " < < SMTRAT_VERSION < < " . " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_CARL
/ / TODO get version string
STORM_PRINT ( " Linked with CArL. " < < std : : endl ) ;
# endif
# ifdef STORM_HAVE_CUDA
int deviceCount = 0 ;
cudaError_t error_id = cudaGetDeviceCount ( & deviceCount ) ;
if ( error_id = = cudaSuccess ) {
STORM_PRINT ( " Compiled with CUDA support, " ) ;
/ / This function call returns 0 if there are no CUDA capable devices .
if ( deviceCount = = 0 ) {
STORM_PRINT ( " but there are no available device(s) that support CUDA. " < < std : : endl ) ;
} else {
STORM_PRINT ( " detected " < < deviceCount < < " CUDA capable device(s): " < < std : : endl ) ;
}
int dev , driverVersion = 0 , runtimeVersion = 0 ;
for ( dev = 0 ; dev < deviceCount ; + + dev ) {
cudaSetDevice ( dev ) ;
cudaDeviceProp deviceProp ;
cudaGetDeviceProperties ( & deviceProp , dev ) ;
STORM_PRINT ( " CUDA device " < < dev < < " : \" " < < deviceProp . name < < " \" " < < std : : endl ) ;
/ / Console log
cudaDriverGetVersion ( & driverVersion ) ;
cudaRuntimeGetVersion ( & runtimeVersion ) ;
STORM_PRINT ( " CUDA Driver Version / Runtime Version " < < driverVersion / 1000 < < " . " < < ( driverVersion % 100 ) / 10 < < " / " < < runtimeVersion / 1000 < < " . " < < ( runtimeVersion % 100 ) / 10 < < std : : endl ) ;
STORM_PRINT ( " CUDA Capability Major/Minor version number: " < < deviceProp . major < < " . " < < deviceProp . minor < < std : : endl ) ;
}
STORM_PRINT ( std : : endl ) ;
}
else {
STORM_PRINT ( " Compiled with CUDA support, but an error occured trying to find CUDA devices. " < < std : : endl ) ;
}
# endif
}
bool parseOptions ( const int argc , const char * argv [ ] ) {
try {
storm : : settings : : mutableManager ( ) . setFromCommandLine ( argc , argv ) ;
} catch ( storm : : exceptions : : OptionParserException & e ) {
storm : : settings : : manager ( ) . printHelp ( ) ;
throw e ;
return false ;
}
storm : : settings : : modules : : GeneralSettings const & general = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) ;
bool result = true ;
if ( general . isHelpSet ( ) ) {
storm : : settings : : manager ( ) . printHelp ( storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) . getHelpModuleName ( ) ) ;
result = false ;
}
if ( general . isVersionSet ( ) ) {
printVersion ( " storm " ) ;
result = false ; ;
}
return result ;
}
void setResourceLimits ( ) {
storm : : settings : : modules : : ResourceSettings const & resources = storm : : settings : : getModule < storm : : settings : : modules : : ResourceSettings > ( ) ;
/ / If we were given a time limit , we put it in place now .
if ( resources . isTimeoutSet ( ) ) {
storm : : utility : : resources : : setCPULimit ( resources . getTimeoutInSeconds ( ) ) ;
}
}
void setLogLevel ( ) {
storm : : settings : : modules : : GeneralSettings const & general = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) ;
storm : : settings : : modules : : DebugSettings const & debug = storm : : settings : : getModule < storm : : settings : : modules : : DebugSettings > ( ) ;
if ( general . isVerboseSet ( ) ) {
storm : : utility : : setLogLevel ( l3pp : : LogLevel : : INFO ) ;
}
if ( debug . isDebugSet ( ) ) {
storm : : utility : : setLogLevel ( l3pp : : LogLevel : : DEBUG ) ;
}
if ( debug . isTraceSet ( ) ) {
storm : : utility : : setLogLevel ( l3pp : : LogLevel : : TRACE ) ;
}
if ( debug . isLogfileSet ( ) ) {
storm : : utility : : initializeFileLogging ( ) ;
}
}
void setFileLogging ( ) {
storm : : settings : : modules : : DebugSettings const & debug = storm : : settings : : getModule < storm : : settings : : modules : : DebugSettings > ( ) ;
if ( debug . isLogfileSet ( ) ) {
storm : : utility : : initializeFileLogging ( ) ;
}
}
void setUrgentOptions ( ) {
setResourceLimits ( ) ;
setLogLevel ( ) ;
setFileLogging ( ) ;
}
struct SymbolicInput {
/ / The symbolic model description .
boost : : optional < storm : : storage : : SymbolicModelDescription > model ;
/ / The properties to check .
std : : vector < storm : : jani : : Property > properties ;
} ;
void parseSymbolicModelDescription ( storm : : settings : : modules : : IOSettings const & ioSettings , SymbolicInput & input ) {
if ( ioSettings . isPrismOrJaniInputSet ( ) ) {
if ( ioSettings . isPrismInputSet ( ) ) {
@ -262,7 +55,7 @@ namespace storm {
auto janiInput = storm : : api : : parseJaniModel ( ioSettings . getJaniInputFilename ( ) ) ;
input . model = janiInput . first ;
auto const & janiPropertyInput = janiInput . second ;
if ( ioSettings . isJaniPropertiesSet ( ) ) {
for ( auto const & propName : ioSettings . getJaniProperties ( ) ) {
auto propertyIt = janiPropertyInput . find ( propName ) ;
@ -273,7 +66,7 @@ namespace storm {
}
}
}
void parseProperties ( storm : : settings : : modules : : IOSettings const & ioSettings , SymbolicInput & input , boost : : optional < std : : set < std : : string > > const & propertyFilter ) {
if ( ioSettings . isPropertySet ( ) ) {
std : : vector < storm : : jani : : Property > newProperties ;
@ -282,30 +75,30 @@ namespace storm {
} else {
newProperties = storm : : api : : parseProperties ( ioSettings . getProperty ( ) , propertyFilter ) ;
}
input . properties . insert ( input . properties . end ( ) , newProperties . begin ( ) , newProperties . end ( ) ) ;
}
}
SymbolicInput parseSymbolicInput ( ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
/ / Parse the property filter , if any is given .
boost : : optional < std : : set < std : : string > > propertyFilter = storm : : api : : parsePropertyFilter ( ioSettings . getPropertyFilter ( ) ) ;
SymbolicInput input ;
parseSymbolicModelDescription ( ioSettings , input ) ;
parseProperties ( ioSettings , input , propertyFilter ) ;
return input ;
}
SymbolicInput preprocessSymbolicInput ( SymbolicInput const & input ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
auto coreSettings = storm : : settings : : getModule < storm : : settings : : modules : : CoreSettings > ( ) ;
SymbolicInput output = input ;
/ / Substitute constant definitions in symbolic input .
std : : string constantDefinitionString = ioSettings . getConstantDefinitionString ( ) ;
std : : map < storm : : expressions : : Variable , storm : : expressions : : Expression > constantDefinitions ;
@ -316,19 +109,19 @@ namespace storm {
if ( ! output . properties . empty ( ) ) {
output . properties = storm : : api : : substituteConstantsInProperties ( output . properties , constantDefinitions ) ;
}
/ / Check whether conversion for PRISM to JANI is requested or necessary .
if ( input . model & & input . model . get ( ) . isPrismProgram ( ) ) {
bool transformToJani = ioSettings . isPrismToJaniSet ( ) ;
bool transformToJaniForJit = coreSettings . getEngine ( ) = = storm : : settings : : modules : : CoreSettings : : Engine : : Sparse & & ioSettings . isJitSet ( ) ;
STORM_LOG_WARN_COND ( transformToJani | | ! transformToJaniForJit , " The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model. " ) ;
transformToJani | = transformToJaniForJit ;
if ( transformToJani ) {
storm : : prism : : Program const & model = output . model . get ( ) . asPrismProgram ( ) ;
auto modelAndRenaming = model . toJaniWithLabelRenaming ( true ) ;
output . model = modelAndRenaming . first ;
if ( ! modelAndRenaming . second . empty ( ) ) {
std : : map < std : : string , std : : string > const & labelRenaming = modelAndRenaming . second ;
std : : vector < storm : : jani : : Property > amendedProperties ;
@ -339,10 +132,10 @@ namespace storm {
}
}
}
return output ;
}
void exportSymbolicInput ( SymbolicInput const & input ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
if ( input . model & & input . model . get ( ) . isJaniModel ( ) ) {
@ -350,23 +143,23 @@ namespace storm {
if ( ioSettings . isExportJaniDotSet ( ) ) {
storm : : api : : exportJaniModelAsDot ( model . asJaniModel ( ) , ioSettings . getExportJaniDotFilename ( ) ) ;
}
if ( model . isJaniModel ( ) & & storm : : settings : : getModule < storm : : settings : : modules : : JaniExportSettings > ( ) . isJaniFileSet ( ) ) {
storm : : api : : exportJaniModel ( model . asJaniModel ( ) , input . properties , storm : : settings : : getModule < storm : : settings : : modules : : JaniExportSettings > ( ) . getJaniFilename ( ) ) ;
}
}
}
SymbolicInput parseAndPreprocessSymbolicInput ( ) {
SymbolicInput input = parseSymbolicInput ( ) ;
input = preprocessSymbolicInput ( input ) ;
exportSymbolicInput ( input ) ;
return input ;
}
std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > createFormulasToRespect ( std : : vector < storm : : jani : : Property > const & properties ) {
std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > result = storm : : api : : extractFormulasFromProperties ( properties ) ;
for ( auto const & property : properties ) {
if ( ! property . getFilter ( ) . getStatesFormula ( ) - > isInitialFormula ( ) ) {
result . push_back ( property . getFilter ( ) . getStatesFormula ( ) ) ;
@ -375,16 +168,24 @@ namespace storm {
return result ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
std : : shared_ptr < storm : : models : : ModelBase > buildModelDd ( SymbolicInput const & input ) {
return storm : : api : : buildSymbolicModel < DdType , ValueType > ( input . model . get ( ) , createFormulasToRespect ( input . properties ) ) ;
return storm : : api : : buildSymbolicModel < DdType , ValueType > ( input . model . get ( ) , createFormulasToRespect ( input . properties ) , storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) . isBuildFullModelSet ( ) ) ;
}
template < typename ValueType >
std : : shared_ptr < storm : : models : : ModelBase > buildModelSparse ( SymbolicInput const & input , storm : : settings : : modules : : IOSettings const & ioSettings ) {
auto counterexampleGeneratorSettings = storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) ;
return storm : : api : : buildSparseModel < ValueType > ( input . model . get ( ) , createFormulasToRespect ( input . properties ) , ioSettings . isBuildChoiceLabelsSet ( ) , counterexampleGeneratorSettings . isMinimalCommandSetGenerationSet ( ) ) ;
storm : : builder : : BuilderOptions options ( createFormulasToRespect ( input . properties ) ) ;
options . setBuildChoiceLabels ( ioSettings . isBuildChoiceLabelsSet ( ) ) ;
options . setBuildChoiceOrigins ( counterexampleGeneratorSettings . isMinimalCommandSetGenerationSet ( ) ) ;
options . setBuildAllLabels ( ioSettings . isBuildFullModelSet ( ) ) ;
options . setBuildAllRewardModels ( ioSettings . isBuildFullModelSet ( ) ) ;
if ( ioSettings . isBuildFullModelSet ( ) ) {
options . clearTerminalStates ( ) ;
}
return storm : : api : : buildSparseModel < ValueType > ( input . model . get ( ) , options , ioSettings . isJitSet ( ) , storm : : settings : : getModule < storm : : settings : : modules : : JitBuilderSettings > ( ) . isDoctorSet ( ) ) ;
}
template < typename ValueType >
@ -416,7 +217,7 @@ namespace storm {
STORM_LOG_THROW ( engine = = storm : : settings : : modules : : CoreSettings : : Engine : : Sparse , storm : : exceptions : : InvalidSettingsException , " Can only use sparse engine with explicit input. " ) ;
result = buildModelExplicit < ValueType > ( ioSettings ) ;
}
modelBuildingWatch . stop ( ) ;
if ( result ) {
STORM_PRINT_AND_LOG ( " Time for model construction: " < < modelBuildingWatch < < " . " < < std : : endl < < std : : endl ) ;
@ -424,7 +225,7 @@ namespace storm {
return result ;
}
template < typename ValueType >
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > preprocessSparseMarkovAutomaton ( std : : shared_ptr < storm : : models : : sparse : : MarkovAutomaton < ValueType > > const & model ) {
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > result = model ;
@ -441,40 +242,40 @@ namespace storm {
if ( bisimulationSettings . isWeakBisimulationSet ( ) ) {
bisimType = storm : : storage : : BisimulationType : : Weak ;
}
STORM_LOG_INFO ( " Performing bisimulation minimization... " ) ;
return storm : : api : : performBisimulationMinimization < ValueType > ( model , createFormulasToRespect ( input . properties ) , bisimType ) ;
}
template < typename ValueType >
std : : pair < std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > , bool > preprocessSparseModel ( std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > const & model , SymbolicInput const & input ) {
auto generalSettings = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) ;
auto bisimulationSettings = storm : : settings : : getModule < storm : : settings : : modules : : BisimulationSettings > ( ) ;
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
std : : pair < std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > , bool > result = std : : make_pair ( model , false ) ;
if ( result . first - > isOfType ( storm : : models : : ModelType : : MarkovAutomaton ) ) {
result . first = preprocessSparseMarkovAutomaton ( result . first - > template as < storm : : models : : sparse : : MarkovAutomaton < ValueType > > ( ) ) ;
result . second = true ;
}
if ( generalSettings . isBisimulationSet ( ) ) {
result . first = preprocessSparseModelBisimulation ( result . first , input , bisimulationSettings ) ;
result . second = true ;
}
return result ;
auto generalSettings = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) ;
auto bisimulationSettings = storm : : settings : : getModule < storm : : settings : : modules : : BisimulationSettings > ( ) ;
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
std : : pair < std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > , bool > result = std : : make_pair ( model , false ) ;
if ( result . first - > isOfType ( storm : : models : : ModelType : : MarkovAutomaton ) ) {
result . first = preprocessSparseMarkovAutomaton ( result . first - > template as < storm : : models : : sparse : : MarkovAutomaton < ValueType > > ( ) ) ;
result . second = true ;
}
if ( generalSettings . isBisimulationSet ( ) ) {
result . first = preprocessSparseModelBisimulation ( result . first , input , bisimulationSettings ) ;
result . second = true ;
}
return result ;
}
template < typename ValueType >
void exportSparseModel ( std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > const & model , SymbolicInput const & input ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
if ( ioSettings . isExportExplicitSet ( ) ) {
storm : : api : : exportSparseModelAsDrn ( model , ioSettings . getExportExplicitFilename ( ) , input . model ? input . model . get ( ) . getParameterNames ( ) : std : : vector < std : : string > ( ) ) ;
}
if ( ioSettings . isExportDotSet ( ) ) {
storm : : api : : exportSparseModelAsDot ( model , ioSettings . getExportDotFilename ( ) ) ;
}
@ -484,7 +285,7 @@ namespace storm {
void exportDdModel ( std : : shared_ptr < storm : : models : : symbolic : : Model < DdType , ValueType > > const & model , SymbolicInput const & input ) {
/ / Intentionally left empty .
}
template < storm : : dd : : DdType DdType , typename ValueType >
void exportModel ( std : : shared_ptr < storm : : models : : ModelBase > const & model , SymbolicInput const & input ) {
if ( model - > isSparseModel ( ) ) {
@ -493,7 +294,7 @@ namespace storm {
exportDdModel < DdType , ValueType > ( model - > as < storm : : models : : symbolic : : Model < DdType , ValueType > > ( ) , input ) ;
}
}
template < storm : : dd : : DdType DdType , typename ValueType >
std : : shared_ptr < storm : : models : : Model < ValueType > > preprocessDdModelBisimulation ( std : : shared_ptr < storm : : models : : symbolic : : Model < DdType , ValueType > > const & model , SymbolicInput const & input , storm : : settings : : modules : : BisimulationSettings const & bisimulationSettings ) {
STORM_LOG_WARN_COND ( ! bisimulationSettings . isWeakBisimulationSet ( ) , " Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation. " ) ;
@ -519,7 +320,7 @@ namespace storm {
template < storm : : dd : : DdType DdType , typename ValueType >
std : : pair < std : : shared_ptr < storm : : models : : ModelBase > , bool > preprocessModel ( std : : shared_ptr < storm : : models : : ModelBase > const & model , SymbolicInput const & input ) {
storm : : utility : : Stopwatch preprocessingWatch ( true ) ;
std : : pair < std : : shared_ptr < storm : : models : : ModelBase > , bool > result = std : : make_pair ( model , false ) ;
if ( model - > isSparseModel ( ) ) {
result = preprocessSparseModel < ValueType > ( result . first - > as < storm : : models : : sparse : : Model < ValueType > > ( ) , input ) ;
@ -529,16 +330,17 @@ namespace storm {
}
preprocessingWatch . stop ( ) ;
if ( result . second ) {
STORM_PRINT_AND_LOG ( std : : endl < < " Time for model preprocessing: " < < preprocessingWatch < < " . " < < std : : endl < < std : : endl ) ;
}
return result ;
}
void printComputingCounterexample ( storm : : jani : : Property const & property ) {
STORM_PRINT_AND_LOG ( " Computing counterexample for property " < < * property . getRawFormula ( ) < < " ... " < < std : : endl ) ;
}
void printCounterexample ( std : : shared_ptr < storm : : counterexamples : : Counterexample > const & counterexample , storm : : utility : : Stopwatch * watch = nullptr ) {
if ( counterexample ) {
STORM_PRINT_AND_LOG ( * counterexample < < std : : endl ) ;
@ -554,17 +356,17 @@ namespace storm {
void generateCounterexamples ( std : : shared_ptr < storm : : models : : ModelBase > const & model , SymbolicInput const & input ) {
STORM_LOG_THROW ( false , storm : : exceptions : : NotSupportedException , " Counterexample generation is not supported for this data-type. " ) ;
}
template < >
void generateCounterexamples < double > ( std : : shared_ptr < storm : : models : : ModelBase > const & model , SymbolicInput const & input ) {
typedef double ValueType ;
STORM_LOG_THROW ( model - > isSparseModel ( ) , storm : : exceptions : : NotSupportedException , " Counterexample generation is currently only supported for sparse models. " ) ;
auto sparseModel = model - > as < storm : : models : : sparse : : Model < ValueType > > ( ) ;
STORM_LOG_THROW ( sparseModel - > isOfType ( storm : : models : : ModelType : : Mdp ) , storm : : exceptions : : NotSupportedException , " Counterexample is currently only supported for MDPs. " ) ;
auto mdp = sparseModel - > template as < storm : : models : : sparse : : Mdp < ValueType > > ( ) ;
auto counterexampleSettings = storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) ;
if ( counterexampleSettings . isMinimalCommandSetGenerationSet ( ) ) {
STORM_LOG_THROW ( input . model & & input . model . get ( ) . isPrismProgram ( ) , storm : : exceptions : : NotSupportedException , " Minimal command set counterexamples are only supported for PRISM model input. " ) ;
@ -587,7 +389,7 @@ namespace storm {
STORM_LOG_THROW ( false , storm : : exceptions : : NotSupportedException , " The selected counterexample formalism is unsupported. " ) ;
}
}
template < typename ValueType >
void printFilteredResult ( std : : unique_ptr < storm : : modelchecker : : CheckResult > const & result , storm : : modelchecker : : FilterType ft ) {
if ( result - > isQuantitative ( ) ) {
@ -641,7 +443,7 @@ namespace storm {
}
STORM_PRINT_AND_LOG ( std : : endl ) ;
}
void printModelCheckingProperty ( storm : : jani : : Property const & property ) {
STORM_PRINT_AND_LOG ( std : : endl < < " Model checking property " < < * property . getRawFormula ( ) < < " ... " < < std : : endl ) ;
}
@ -660,25 +462,25 @@ namespace storm {
STORM_PRINT_AND_LOG ( " failed, property is unsupported by selected engine/settings. " < < std : : endl ) ;
}
}
struct PostprocessingIdentity {
void operator ( ) ( std : : unique_ptr < storm : : modelchecker : : CheckResult > const & ) {
/ / Intentionally left empty .
}
} ;
template < typename ValueType >
void verifyProperties ( std : : vector < storm : : jani : : Property > const & properties , std : : function < std : : unique_ptr < storm : : modelchecker : : CheckResult > ( std : : shared_ptr < storm : : logic : : Formula const > const & formula , std : : shared_ptr < storm : : logic : : Formula const > const & states ) > const & verificationCallback , std : : function < void ( std : : unique_ptr < storm : : modelchecker : : CheckResult > const & ) > const & postprocessingCallback = PostprocessingIdentity ( ) ) {
for ( auto const & property : properties ) {
printModelCheckingProperty ( property ) ;
storm : : utility : : Stopwatch watch ( true ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > result = verificationCallback ( property . getRawFormula ( ) , property . getFilter ( ) . getStatesFormula ( ) ) ;
watch . stop ( ) ;
postprocessingCallback ( result ) ;
printResult < ValueType > ( result , property , & watch ) ;
}
for ( auto const & property : properties ) {
printModelCheckingProperty ( property ) ;
storm : : utility : : Stopwatch watch ( true ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > result = verificationCallback ( property . getRawFormula ( ) , property . getFilter ( ) . getStatesFormula ( ) ) ;
watch . stop ( ) ;
postprocessingCallback ( result ) ;
printResult < ValueType > ( result , property , & watch ) ;
}
}
template < storm : : dd : : DdType DdType , typename ValueType >
void verifyWithAbstractionRefinementEngine ( SymbolicInput const & input ) {
STORM_LOG_ASSERT ( input . model , " Expected symbolic model description. " ) ;
@ -697,7 +499,7 @@ namespace storm {
return storm : : api : : verifyWithExplorationEngine < ValueType > ( input . model . get ( ) , storm : : api : : createTask < ValueType > ( formula , true ) ) ;
} ) ;
}
template < typename ValueType >
void verifyWithSparseEngine ( std : : shared_ptr < storm : : models : : ModelBase > const & model , SymbolicInput const & input ) {
auto sparseModel = model - > as < storm : : models : : sparse : : Model < ValueType > > ( ) ;
@ -706,7 +508,7 @@ namespace storm {
bool filterForInitialStates = states - > isInitialFormula ( ) ;
auto task = storm : : api : : createTask < ValueType > ( formula , filterForInitialStates ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > result = storm : : api : : verifyWithSparseEngine < ValueType > ( sparseModel , task ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > filter ;
if ( filterForInitialStates ) {
filter = std : : make_unique < storm : : modelchecker : : ExplicitQualitativeCheckResult > ( sparseModel - > getInitialStates ( ) ) ;
@ -725,10 +527,10 @@ namespace storm {
verifyProperties < ValueType > ( input . properties , [ & model ] ( std : : shared_ptr < storm : : logic : : Formula const > const & formula , std : : shared_ptr < storm : : logic : : Formula const > const & states ) {
bool filterForInitialStates = states - > isInitialFormula ( ) ;
auto task = storm : : api : : createTask < ValueType > ( formula , filterForInitialStates ) ;
auto symbolicModel = model - > as < storm : : models : : symbolic : : Model < DdType , ValueType > > ( ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > result = storm : : api : : verifyWithHybridEngine < DdType , ValueType > ( symbolicModel , task ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > filter ;
if ( filterForInitialStates ) {
filter = std : : make_unique < storm : : modelchecker : : SymbolicQualitativeCheckResult < DdType > > ( symbolicModel - > getReachableStates ( ) , symbolicModel - > getInitialStates ( ) ) ;
@ -788,11 +590,36 @@ namespace storm {
verifySymbolicModel < DdType , ValueType > ( model , input , coreSettings ) ;
}
}
template < storm : : dd : : DdType DdType , typename ValueType >
std : : shared_ptr < storm : : models : : ModelBase > buildPreprocessExportModelWithValueTypeAndDdlib ( SymbolicInput const & input , storm : : settings : : modules : : CoreSettings : : Engine engine ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
std : : shared_ptr < storm : : models : : ModelBase > model ;
if ( ! ioSettings . isNoBuildModelSet ( ) ) {
model = buildModel < DdType , ValueType > ( engine , input , ioSettings ) ;
}
if ( model ) {
model - > printModelInformationToStream ( std : : cout ) ;
}
STORM_LOG_THROW ( model | | input . properties . empty ( ) , storm : : exceptions : : InvalidSettingsException , " No input model. " ) ;
if ( model ) {
auto preprocessingResult = preprocessModel < DdType , ValueType > ( model , input ) ;
if ( preprocessingResult . second ) {
model = preprocessingResult . first ;
model - > printModelInformationToStream ( std : : cout ) ;
}
exportModel < DdType , ValueType > ( model , input ) ;
}
return model ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
void processInputWithValueTypeAndDdlib ( SymbolicInput const & input ) {
auto coreSettings = storm : : settings : : getModule < storm : : settings : : modules : : CoreSettings > ( ) ;
/ / For several engines , no model building step is performed , but the verification is started right away .
storm : : settings : : modules : : CoreSettings : : Engine engine = coreSettings . getEngine ( ) ;
if ( engine = = storm : : settings : : modules : : CoreSettings : : Engine : : AbstractionRefinement ) {
@ -800,43 +627,24 @@ namespace storm {
} else if ( engine = = storm : : settings : : modules : : CoreSettings : : Engine : : Exploration ) {
verifyWithExplorationEngine < ValueType > ( input ) ;
} else {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
std : : shared_ptr < storm : : models : : ModelBase > model ;
if ( ! ioSettings . isNoBuildModelSet ( ) ) {
model = buildModel < DdType , ValueType > ( engine , input , ioSettings ) ;
}
if ( model ) {
model - > printModelInformationToStream ( std : : cout ) ;
}
STORM_LOG_THROW ( model | | input . properties . empty ( ) , storm : : exceptions : : InvalidSettingsException , " No input model. " ) ;
if ( model ) {
auto preprocessingResult = preprocessModel < DdType , ValueType > ( model , input ) ;
if ( preprocessingResult . second ) {
model = preprocessingResult . first ;
model - > printModelInformationToStream ( std : : cout ) ;
}
}
std : : shared_ptr < storm : : models : : ModelBase > model = buildPreprocessExportModelWithValueTypeAndDdlib < DdType , ValueType > ( input , engine ) ;
if ( model ) {
exportModel < DdType , ValueType > ( model , input ) ;
if ( coreSettings . isCounterexampleSet ( ) ) {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
generateCounterexamples < ValueType > ( model , input ) ;
} else {
auto ioSettings = storm : : settings : : getModule < storm : : settings : : modules : : IOSettings > ( ) ;
verifyModel < DdType , ValueType > ( model , input , coreSettings ) ;
}
}
}
}
template < typename ValueType >
void processInputWithValueType ( SymbolicInput const & input ) {
auto coreSettings = storm : : settings : : getModule < storm : : settings : : modules : : CoreSettings > ( ) ;
if ( coreSettings . getDdLibraryType ( ) = = storm : : dd : : DdType : : CUDD ) {
processInputWithValueTypeAndDdlib < storm : : dd : : DdType : : CUDD , ValueType > ( input ) ;
} else {
@ -844,53 +652,6 @@ namespace storm {
processInputWithValueTypeAndDdlib < storm : : dd : : DdType : : Sylvan , ValueType > ( input ) ;
}
}
void processOptions ( ) {
/ / Start by setting some urgent options ( log levels , resources , etc . )
setUrgentOptions ( ) ;
/ / Parse and preprocess symbolic input ( PRISM , JANI , properties , etc . )
SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput ( ) ;
auto generalSettings = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) ;
if ( generalSettings . isParametricSet ( ) ) {
# ifdef STORM_HAVE_CARL
processInputWithValueType < storm : : RationalFunction > ( symbolicInput ) ;
# else
STORM_LOG_THROW ( false , storm : : exceptions : : NotSupportedException , " No parameters are supported in this build. " ) ;
# endif
} else if ( generalSettings . isExactSet ( ) ) {
# ifdef STORM_HAVE_CARL
processInputWithValueType < storm : : RationalNumber > ( symbolicInput ) ;
# else
STORM_LOG_THROW ( false , storm : : exceptions : : NotSupportedException , " No exact numbers are supported in this build. " ) ;
# endif
} else {
processInputWithValueType < double > ( symbolicInput ) ;
}
}
void printTimeAndMemoryStatistics ( uint64_t wallclockMilliseconds ) {
struct rusage ru ;
getrusage ( RUSAGE_SELF , & ru ) ;
std : : cout < < std : : endl < < " Performance statistics: " < < std : : endl ;
# ifdef MACOS
/ / For Mac OS , this is returned in bytes .
uint64_t maximumResidentSizeInMegabytes = ru . ru_maxrss / 1024 / 1024 ;
# endif
# ifdef LINUX
/ / For Linux , this is returned in kilobytes .
uint64_t maximumResidentSizeInMegabytes = ru . ru_maxrss / 1024 ;
# endif
std : : cout < < " * peak memory usage: " < < maximumResidentSizeInMegabytes < < " MB " < < std : : endl ;
char oldFillChar = std : : cout . fill ( ' 0 ' ) ;
std : : cout < < " * CPU time: " < < ru . ru_utime . tv_sec < < " . " < < std : : setw ( 3 ) < < ru . ru_utime . tv_usec / 1000 < < " s " < < std : : endl ;
if ( wallclockMilliseconds ! = 0 ) {
std : : cout < < " * wallclock time: " < < ( wallclockMilliseconds / 1000 ) < < " . " < < std : : setw ( 3 ) < < ( wallclockMilliseconds % 1000 ) < < " s " < < std : : endl ;
}
std : : cout . fill ( oldFillChar ) ;
}
}
}
}
dehnert
8 years ago