{CHOICE_TYPE,PRISM_ENGINE,"Engine","3.0","Hybrid","MTBDD,Sparse,Hybrid","Which engine (hybrid, sparse or MTBDD) should be used for model checking."},
{BOOLEAN_TYPE,PRISM_VERBOSE,"Verbose output","3.0",newBoolean(false),"","Display verbose output to log."},
{BOOLEAN_TYPE,PRISM_FAIRNESS,"Use fairness","3.0",newBoolean(false),"","Constrain to fair adversaries when model checking MDPs."},
{BOOLEAN_TYPE,PRISM_FAIRNESS,"Use fairness","3.0",newBoolean(false),"","Constrain to fair adversaries when model checking probabilistic reachability properties of MDPs."},
{BOOLEAN_TYPE,PRISM_PRECOMPUTATION,"Use precomputation","3.0",newBoolean(true),"","Use model checking precomputation algorithms (Prob0, Prob1, etc.)."},
{BOOLEAN_TYPE,PRISM_DO_PROB_CHECKS,"Do probability/rate checks","3.0",newBoolean(true),"","Perform sanity checks on model probabilities/rates when constructing probabilistic models."},
{BOOLEAN_TYPE,PRISM_COMPACT,"Use compact schemes","3.0",newBoolean(true),"","Use additional optimisations for compressing sparse matrices and vectors with repeated values."},