imperialqore/line-prism-rest repository overview

⁠line-prism-rest (Docker image)

REST packaging of the PRISM probabilistic model checker, for use as an external solver of the LINE solver⁠.

All credit for PRISM belongs to its authors. This image contributes no method, no algorithm and no result: it adds a batch driver and exposes the upstream tool over HTTP. Upstream project: https://www.prismmodelchecker.org/⁠ and https://github.com/prismmodelchecker/prism⁠.

PRISM already has a command line, bin/prism. This image adds a different one, because the existing one is awkward to call from another solver:

• Model-checking failures are not fatal to bin/prism: PrismCL.error() prints Error: ... and the process still exits 0, so a caller cannot distinguish success from failure by exit code. Here, failure sets both the exit code and a status field in the JSON output.
• One LINE query is many PRISM queries. Filling an M x K grid of mean queue lengths, utilizations and throughputs takes 3*M*K steady-state reward queries. This driver takes them as a batch and builds the state space once, instead of once per process launch.
• PRISM's default linear-equation method, Jacobi, fails to converge within its default 10000 iterations on chains as small as an M/M/1/5. The default here is Gauss-Seidel with a 1e-9 relative tolerance.

⁠Usage

⁠REST server (default)

docker run --rm -p 8080:8080 imperialqore/line-prism-rest
curl -s http://127.0.0.1:8080/api/v1/health

⁠Command line

docker run --rm -v "$PWD:/data" imperialqore/line-prism-rest job.json

The container reads the job and its model files from /data and writes JSON to stdout. PRISM's narration goes to stderr, so stdout can be piped straight into a JSON parser. Options: --out FILE, --engine mtbdd|sparse|hybrid|explicit, --timeout SECONDS, --version.

⁠API

Base path /api/v1.

⁠The job format

A PRISM model file:

{
  "format": "prism",
  "modelType": "ctmc",
  "model": "mm1k.sm",
  "consts": {"K": 5},
  "queries": [
    {"id": "Q_1_1", "reward": "Q_1_1"},
    {"id": "p_full", "prop": "S=? [ n = K ]"}
  ]
}

or an explicit model, which is how LINE hands over a generator it has already built:

{
  "format": "explicit",
  "modelType": "ctmc",
  "trans": "model.tra", "states": "model.sta", "labels": "model.lab",
  "stateRewards": ["Q_1_1.srew", "U_1_1.srew", "T_1_1.srew"],
  "queries": [{"id": "Q_1_1", "reward": "Q_1_1"}],
  "exportSteadyState": true
}

A query names either a reward structure (reward, expanded to R{"name"}=? [ S ], its long-run expectation), a 1-based reward index (rewardIndex, for explicit imports whose reward files carry no name), or a raw PRISM property (prop). Optional job fields: engine, linEqMethod, epsilon, maxIters, exportSteadyState.

⁠Credits

All credit for PRISM belongs to its authors. This project only packages it. If you publish results obtained through this service, cite the PRISM authors. Do not cite this image or the packaging repository.

PRISM is developed by Marta Kwiatkowska, Gethin Norman and David Parker, at the University of Oxford and the University of Glasgow.

The PRISM project presents the following as its tool paper:

The running service returns this attribution at GET /api/v1/citation, so the credit travels with the results.

⁠Licence

PRISM is GPL v2. The driver links PRISM in-process and is therefore a derivative work, distributed under the same licence.

Upstream project: https://www.prismmodelchecker.org/⁠, https://github.com/prismmodelchecker/prism⁠

Packaged for: https://line-solver.sourceforge.net/⁠