Data formats

write_prism_file(path_without_file_ending, problem)

Write the files required by PRISM explicit engine/format to

• path_without_file_ending.sta (states),
• path_without_file_ending.lab (labels),
• path_without_file_ending.tra (transitions), and
• path_without_file_ending.pctl (properties).

If the specification is a reward optimization problem, then a state rewards file .srew is also written.

See Data storage formats for more information on the file format.

read_prism_file(path_without_file_ending)

Read PRISM explicit file formats and pctl file, and return a ControlSynthesisProblem including system and specification.

See PRISM Explicit Model Files for more information on the file format.

read_bmdp_tool_file(path)

Read a bmdp-tool transition probability file and return an IntervalMarkovDecisionProcess and a list of terminal states. From the file format, it is not clear if the desired reachability verification if the reachability specification is finite or infinite horizon, the satisfaction_mode is pessimistic or optimistic, or if the actions should minimize or maximize the probability of reachability.

See Data storage formats for more information on the file format.

write_bmdp_tool_file(path, problem::IntervalMDP.AbstractIntervalMDPProblem)

Write a bmdp-tool transition probability file for the given an IMDP and a reachability specification. The file will not contain enough information to specify a reachability specification. The remaining parameters are rather command line arguments.

See Data storage formats for more information on the file format.

write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, spec::Specification)

write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, prop::AbstractReachability)

write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, terminal_states::Vector{T})

write_bmdp_tool_file(path, mdp::IntervalMarkovDecisionProcess, terminal_states::Vector{<:CartesianIndex})

read_intervalmdp_jl(model_path, spec_path; control_synthesis = false)

Read an IntervalMDP.jl data file and return a ControlSynthesisProblem or VerificationProblem depending on the control_synthesis flag.

See Data storage formats for more information on the file format.

read_intervalmdp_jl_model(model_path)

Read an IntervalMarkovDecisionProcess or IntervalMarkovChain from an IntervalMDP.jl system file (netCDF sparse format).

See Data storage formats for more information on the file format.

read_intervalmdp_jl_spec(spec_path)

Read a Specification from an IntervalMDP.jl spec file (JSON-format).

See Data storage formats for more information on the file format.

write_intervalmdp_jl_model(model_path, mdp)

Write an IntervalMarkovDecisionProcess to an IntervalMDP.jl system file (netCDF sparse format).

See Data storage formats for more information on the file format.

write_intervalmdp_jl_spec(spec_path, spec::Specification)

Write a Specification to an IntervalMDP.jl spec file (JSON-format).

See Data storage formats for more information on the file format.