prophesy package

Subpackages

• prophesy.data package
  • Submodules
    • prophesy.data.constant module
    • prophesy.data.constraint module
    • prophesy.data.hyperrectangle module
    • prophesy.data.interval module
    • prophesy.data.model_type module
    • prophesy.data.nice_approximation module
    • prophesy.data.parameter module
    • prophesy.data.point module
    • prophesy.data.property module
    • prophesy.data.range module
    • prophesy.data.samples module
• prophesy.regions package
  • Module contents
  • Region Checking
    • prophesy.regions.region_checker module
    • prophesy.regions.region_smtchecker module
  • Region Generation
    • prophesy.regions.region_generation module
    • prophesy.regions.region_quads module
• prophesy.sampling package
  • Sampler: How to sample?
    • prophesy.sampling.sampler module
    • prophesy.sampling.sampler_ratfunc module
    • Sampling via probabilistic model checking
  • Sampling: Where to sample?
    • prophesy.sampling.sample_generator module
    • prophesy.sampling.sampling_linear module
    • prophesy.sampling.sampling_uniform module
  • High-level convenience functions
    • prophesy.sampling.sampling module
• prophesy.modelcheckers package
  • Module contents
  • Interfaces
    • prophesy.modelcheckers.pmc module
    • prophesy.modelcheckers.ppmc module
  • Implementations
    • prophesy.modelcheckers.storm module
    • prophesy.modelcheckers.stormpy module
    • prophesy.modelcheckers.param module
    • prophesy.modelcheckers.prism module
• prophesy.smt package
  • Interfaces and convenience functions
    • prophesy.smt.smt module
    • prophesy.smt.smtlib module
  • Solver bindings
    • prophesy.smt.Z3cli_solver module
    • prophesy.smt.YicesCli_solver module
    • prophesy.smt.isat module
  • Module contents
• prophesy.exceptions package
• prophesy.input package
  • Input file handlers
    • prophesy.input.modelfile module
    • prophesy.input.pctlfile module
    • prophesy.input.problem_description module
    • prophesy.input.samplefile module
    • prophesy.input.solutionfunctionfile module
• prophesy.output package
  • prophesy.output.plot module

Utility methods

prophesy.util module

class prophesy.util.Configuration(config_file)

Bases: object

Configuration for prophesy.

check_existence(section, key)

Check if the given key exists in the configuration and raise a ConfigurationError if not. :param section: Section. :param key: Key.

get(section, key)

Get config value for given key. :param section: Section. :param key: Key. :return: Config value.

get_all()

Get all entries of the configuration. :return: Dict with all entries.

get_boolean(section, key)

Get config value as boolean. :param section: Section. :param key: Key. :return: Config value as boolean.

get_float(section, key)

Get config value as float. :param section: Section. :param key: Key. :return: Config value as float.

get_int(section, key)

Get config value as integer. :param section: Section. :param key: Key. :return: Config value as integer.

set(section, key, value)

Set config entry. :param section: Section. :param key: Key. :param value: New value.

update_configuration_file()

Write configuration file again.

prophesy.util.check_filepath_for_reading(filepath, filedescription_string='file')

Check if the given path can be read. Raises an IOError otherwise. :param filepath: Path. :param filedescription_string: Type of path (file/dir).

prophesy.util.ensure_dir_exists(path)

Check whether the directory exists and create it if not. Raises an IOError if not successful. :param path: Directory path.

prophesy.util.open_file(path)

Open file with system-default application. Works for Mac OS (open) and Linux with xdg-open. :param path: Path.

prophesy.util.run_tool(args, quiet=False, outputfile=None)

Executes a process. :param args: CLI arguments to execute. :param quiet: If false the output is logged. :param outputfile: Path for saving output. :return: Stdout of process or exitcode.

prophesy.util.which(program)

Check if executable exists and return its path. See http://stackoverflow.com/questions/377017/test-if-executable-exists-in-python/377028#377028 :param program: String with name of the program. :return: Path to program or None if not found.

prophesy.util.write_string_to_file(path, string, append=False)

Write string to file. :param path: File where we want to put the string. :param string: New content. :param append: If True, append to file, else overwrite.

prophesy.util.write_string_to_tmpfile(string)

Write string to temporary file. :param string: New content. :return: The path to the temporary file.

prophesy.config module

class prophesy.config.ModulesConfig

Bases: prophesy.util.Configuration

DEPENDENCIES = 'installed_deps'

has_pycarl_parser()

has_stormpy()

is_module_available(module)

class prophesy.config.ProphesyConfig(path_to_cfg)

Bases: prophesy.util.Configuration

CONSTRAINTS = 'constraints'

DIRECTORIES = 'directories'

EXTERNAL_TOOLS = 'external_tools'

SAMPLING = 'sampling'

SMT = 'smt'

check_tools()

getAvailableParametricMCs()

Returns:A set with strings describing the available parametric pmcs.

getAvailableProbMCs()

getAvailableSMTSolvers()

getAvailableSamplers()

getSection(sec)

get_intermediate_dir()

get_isat()

get_param()

get_plots_dir()

get_prism()

get_sampling_epsilon()

get_sampling_min_distance()

get_smt_memout()

get_smt_timeout()

get_storm()

get_storm_pars()

get_tool(toolname)

get_yices()

get_z3()

has_gurobipy()

has_stormpy()

prophesy.config.load_configuration(path=None)