prophesy.input package¶

Input file handlers¶

prophesy.input.modelfile module¶

class DrnFile(location, do_transform=False)¶

Bases: prophesy.input.modelfile.ModelInput

Wraps a DRN file.

contains_nondeterministic_model()¶

class ModelInput(do_transform=False)¶

Bases: object

Abstract class for input model descriptions.

class PrismFile(location, do_transform=False)¶

Bases: prophesy.input.modelfile.ModelInput

Wrapper for Prism file; extracts parameter names.

Rationale for not using stormpy bindings: Support for prism file should be given even without stormpy.

contains_nondeterministic_model()¶

make_temporary_copy()¶: Makes a temporary copy of itself, which will be deleted automatically. Does nothing if a temporary copy already exists.

nr_parameters()¶

replace_parameter_keyword(new_keyword)¶: Substitutes parameter type keywords (e.g. ‘const double’) with the given string (unless the line is commented out).

open_model_file(location)¶

prophesy.input.pctlfile module¶

class PctlFile(location)¶

Bases: object

Wrapper for pctl files, which contain a list of pctl formulae

get(index)¶

get_nr_formulas()¶

prophesy.input.problem_description module¶

class PctlFile(location)¶

Bases: object

Wrapper for pctl files, which contain a list of pctl formulae

get(index)¶

get_nr_formulas()¶

prophesy.input.samplefile module¶

read_samples_file(path, parameters)¶

Reads sample files.

The first line specifies the parameters (with an optional “Result” for the last column). The second line optionally specifies a threshold. This is important if we have binary samples, (for which we do not know the value, but just whether it is above or below the threshold). The remaining lines give the parameter values and the value. This value is either a number or “above” or “below”.

Parameters: path –
Returns

write_samples_file(parameters, samples, path)¶

prophesy.input.solutionfunctionfile module¶

class ParametricResult(parameters, parameter_constraints, graph_preservation_constraints, ratfunc)¶

Bases: object

Stores the data that represent a property of a parametric model, which are its parameters, the solution function for the property and any constraints that apply to the parameters.

read_param_result(location)¶

read_pstorm_result(location, require_result=True)¶: Read the output of pstorm into a ParametricResult :param location: The location of the file to be read :type location: str :param require_result: If true, parsing fails if no result is found :type require_result: Bool :return: The data obtained from the model. :rtype: ParametricResult

write_pstorm_result(location, result)¶