@ -1056,6 +1056,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
/ * * / * *
* Get ( exclusive ) access to the PRISM parser . * Get ( exclusive ) access to the PRISM parser .
* Not usually used externally - use the ready - made model / property parse methods instead .
* / * /
public static PrismParser getPrismParser ( ) throws InterruptedException public static PrismParser getPrismParser ( ) throws InterruptedException
{ {
@ -1566,8 +1567,19 @@ public class Prism extends PrismComponent implements PrismSettingsListener
} }
/ * * / * *
* Parse a PRISM properties file . Typically , you need to pass in some info about the corresponding model
* ( for access to constants , etc . ) . This is in the form of a ModelInfo object ( e . g . a ModulesFile ) . If not required , this can be null .
* Parse a PRISM properties file , using the currently loaded model
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* @param file File to read in
* /
public PropertiesFile parsePropertiesFile ( File file ) throws FileNotFoundException , PrismLangException
{
return parsePropertiesFile ( currentModelInfo , file , true ) ;
}
/ * *
* Parse a PRISM properties file , using a specific ModelInfo object ( e . g . ModulesFile )
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* Usually , just use { @link # parsePropertiesFile ( File ) } , which uses the currently loaded model .
* @param modelInfo Accompanying model info ( null if not needed ) * @param modelInfo Accompanying model info ( null if not needed )
* @param file File to read in * @param file File to read in
* / * /
@ -1577,10 +1589,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener
} }
/ * * / * *
* Parse a PRISM properties file . Typically , you need to pass in some info about the corresponding model
* ( for access to constants , etc . ) . This is in the form of a ModelInfo object ( e . g . a ModulesFile ) . If not required , this can be null .
* Parse a PRISM properties file , using the currently loaded model
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* You can also choose whether to do "tidy" , i . e . post - parse checks and processing * You can also choose whether to do "tidy" , i . e . post - parse checks and processing
* ( this must be done at some point but may want to postpone to allow parsing of files with errors ) . * ( this must be done at some point but may want to postpone to allow parsing of files with errors ) .
* @param file File to read in
* @param tidy Whether or not to do "tidy" ( post - parse checks and processing )
* /
public PropertiesFile parsePropertiesFile ( File file , boolean tidy ) throws FileNotFoundException , PrismLangException
{
return parsePropertiesFile ( currentModelInfo , file , tidy ) ;
}
/ * *
* Parse a PRISM properties file , using a specific ModelInfo object ( e . g . ModulesFile )
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* You can also choose whether to do "tidy" , i . e . post - parse checks and processing
* ( this must be done at some point but may want to postpone to allow parsing of files with errors ) .
* Usually , just use { @link # parsePropertiesFile ( File , boolean ) } , which uses the currently loaded model .
* @param modelInfo Accompanying model info ( null if not needed ) * @param modelInfo Accompanying model info ( null if not needed )
* @param file File to read in * @param file File to read in
* @param tidy Whether or not to do "tidy" ( post - parse checks and processing ) * @param tidy Whether or not to do "tidy" ( post - parse checks and processing )
@ -1616,8 +1642,19 @@ public class Prism extends PrismComponent implements PrismSettingsListener
} }
/ * * / * *
* Parse a PRISM properties file form a string . Typically , you need to pass in some info about the corresponding model
* ( for access to constants , etc . ) . This is in the form of a ModelInfo object ( e . g . a ModulesFile ) . If not required , this can be null .
* Parse a PRISM properties file from a string , using the currently loaded model
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* @param s String to parse
* /
public PropertiesFile parsePropertiesString ( String s ) throws PrismLangException
{
return parsePropertiesString ( currentModelInfo , s ) ;
}
/ * *
* Parse a PRISM properties file from a string , using a specific ModelInfo object ( e . g . ModulesFile )
* for context ( i . e . definitions of variables , constants , labels , etc . ) .
* Usually , just use { @link # parsePropertiesString ( String ) } , which uses the currently loaded model .
* @param modelInfo Accompanying model info ( null if not needed ) * @param modelInfo Accompanying model info ( null if not needed )
* @param s String to parse * @param s String to parse
* / * /
@ -2139,7 +2176,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
} }
/ * / / Create new model checker object and do model checking / * / / Create new model checker object and do model checking
PropertiesFile pf = parsePropertiesString ( currentModelInfo , "filter(exists,!\"invariants\"); E[F!\"invariants\"]" ) ;
PropertiesFile pf = parsePropertiesString ( "filter(exists,!\"invariants\"); E[F!\"invariants\"]" ) ;
if ( ! getExplicit ( ) ) { if ( ! getExplicit ( ) ) {
ModelChecker mc = new NondetModelChecker ( this , currentModel , pf ) ; ModelChecker mc = new NondetModelChecker ( this , currentModel , pf ) ;
if ( ( ( Boolean ) mc . check ( pf . getProperty ( 0 ) ) . getResult ( ) ) . booleanValue ( ) ) { if ( ( ( Boolean ) mc . check ( pf . getProperty ( 0 ) ) . getResult ( ) ) . booleanValue ( ) ) {
@ -2871,7 +2908,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
* / * /
public Result modelCheck ( String propertyString ) throws PrismException public Result modelCheck ( String propertyString ) throws PrismException
{ {
PropertiesFile propertiesFile = parsePropertiesString ( currentModelInfo , propertyString ) ;
PropertiesFile propertiesFile = parsePropertiesString ( propertyString ) ;
if ( propertiesFile . getNumProperties ( ) ! = 1 ) { if ( propertiesFile . getNumProperties ( ) ! = 1 ) {
throw new PrismException ( "There should be exactly one property to check (there are " + propertiesFile . getNumProperties ( ) + ")" ) ; throw new PrismException ( "There should be exactly one property to check (there are " + propertiesFile . getNumProperties ( ) + ")" ) ;
} }
@ -3794,7 +3831,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
/ / Create a dummy properties file if none exist / / Create a dummy properties file if none exist
/ / ( the symbolic model checkers rely on this to store e . g . model labels ) / / ( the symbolic model checkers rely on this to store e . g . model labels )
if ( propertiesFile = = null ) { if ( propertiesFile = = null ) {
propertiesFile = parsePropertiesString ( currentModelInfo , "" ) ;
propertiesFile = parsePropertiesString ( "" ) ;
} }
/ / Create model checker / / Create model checker
StateModelChecker mc = StateModelChecker . createModelChecker ( currentModelType , this , currentModel , propertiesFile ) ; StateModelChecker mc = StateModelChecker . createModelChecker ( currentModelType , this , currentModel , propertiesFile ) ;
Dave Parker
7 years ago