Skip to content

Model export/import improvements, including headers and combined .pexp format#290

Merged
davexparker merged 19 commits into
prismmodelchecker:masterfrom
davexparker:export+import
Jul 14, 2026
Merged

Model export/import improvements, including headers and combined .pexp format#290
davexparker merged 19 commits into
prismmodelchecker:masterfrom
davexparker:export+import

Conversation

@davexparker

@davexparker davexparker commented Jul 14, 2026 •
edited
Loading

Copy link
Copy Markdown
Member
  • Explicit model files now include a commented header by default
  • For .tra file, header includes the model type, which is read on import
  • Import/export of combined explicit model files, default extension .pexp
  • Import/export of zipped explicit model files

davexparker added 15 commits July 2, 2026 11:38
@davexparker
Clarify when deadlocks are included in model export.
d46ddd9 
* always included in explicit (.lab) format
* for UMB, omit if there are no deadlocks
* DRN does not show labels if missing anyway
@davexparker
Importer for explicit model format ignores irrelevant lines starting #.
5e8f829 
Apart from rewards, where these lines are processed to extract
reward structure names, most import code was already supposed to
ignore "comment" lines starting with #. But in fact, various methods
for file processing did not do so. This is now fixed.

Shortly, headers will be added to exports more widely. This will allow
the current code to ignore them on import.
@davexparker
Explicit format headers + combined export format (.pexp).
eaba9c2 
All explicit model exports (.tra, .sta, etc.) now include a
commented header line, as was already the case for rewards.
For .tra, this also indicates the model type, e.g.:

As before for rewards, this can be turned off by adding the
option headers=false to -exportmodel. The headers=true/false
option is also added to individual -exporttrans, etc.

Currently, apart from rewards, lines beginning # are ignored
by the model importing code anyway, so the generated files
with headers can be read back into PRISM without problem.

A new single-file explicit format export is also added, with
all content (.tra, .sta, .lab, .*rew, .obs) included in the
same file, and separated by headers. The default extension for
this is .pexp ("PRISM explicit"). Export is supported for
both explicit and symbolic engines.

The single-file format becomes the default for -exportmodel
if no recognised file extension is used, so e.g. the following
all output all parts of the model:

 prism model.prism -exportmodel stdout
 prism model.prism -exportmodel model.txt
 prism model.prism -exportmodel stdout.pexp

If you want just the transitions, use file extension .tra or
use any extension and turn off the other model entities:

 prism model.prism -exportmodel stdout.tra
 prism model.prism -exportmodel stdout:states=false,labels=false,rewards=false

To enable symbolic export, the C++ exporting code has some changes
in the calling arguments. The sparse and MTBDD C++ export functions
gain an append parameter so successive sections can be appended
to the same file without reopening in write mode. ModelExportOptions
gains appendToFile, used to trigger this.

All import/export regression tests are updated to the new format.
New regression tests for .pexp format on all models are also added.
@davexparker
Import of combined explicit model format (.pexp).
bf1b515 
Adds -importmodel support for the .pexp combined single-file format,
the import-side counterpart to the -exportmodel .pexp export added
in the previous commit.

Like .all, "-importmodel" can be omitted for .pexp.

PrismExplicitImporter is extended with FileSection (an internal class
storing a file plus a line range) and LineBoundedReader (a Reader
subclass that yields at most N lines from a positioned BufferedReader
before reporting EOF). All internal File fields become FileSection;
the existing per-file API (setStatesFile etc.) is unchanged. A new
addCombinedFile(File) method does a single scan pass to locate section
headers in any order, then maps each section to a bounded FileSection.
The transitions section header is optional: if absent the whole file
(or the prefix up to the first recognised header) is treated as the
transitions section, so a plain .tra file can be passed to
addCombinedFile without error.

PrismCL is extended to dispatch .pexp to addCombinedFile in
sortModelImports, and rejects .pexp combined with other -import*
switches (like UMB).
@davexparker
Improved handling of # comments and headers in explicit model file im…
139a2dc 
…port.

When importing explicit model files (.tra, .sta, .lab, .srew, .trew, .pexp):

- If a file starts with a # header comment, it is validated against the
  expected section type; a header-like comment for the wrong section (e.g.
  "# Labels" at the start of a .tra file) gives a clear error message
  instead of a cryptic parse failure downstream.
- The model type in the transitions file header (e.g. "# Transitions (DTMC)")
  is now used to determine the model type, taking priority over auto-detection
  from data shape but not over a user-supplied type override. An unrecognised
  type name in the header is an error.
- In combined .pexp files, an unrecognised # line that looks like a mistyped
  section header (single word, letters/parens only, e.g. "# State") is now
  flagged with a clear error. Plain # comments (e.g. "# 3 5 0.5") are still
  silently ignored.
- # comment lines are now skipped throughout all data sections of every
  explicit model file, not just at the top, restoring support for commenting
  out individual data lines.
@davexparker
Fix reward data loss on in-place importmodel+exportmodel round-trip.
ecb1034 
When the export target has the same path as the import source (e.g. the
-importmodel X.all -exportmodel X.all form), state/transition reward
data for numbered reward structures (e.g. lec9ctl11.srew) was silently
zeroed out. Root cause: in exportStateRewards() and exportTransRewards(),
the output file was opened (and truncated) via getPrismLogForFile() *before*
constructRewards() was called. Reward data from explicit import files is
read lazily - PrismExplicitImporter opens a fresh FileReader on the source
file only when constructRewards() actually executes. When source and
destination share a path, the truncate-on-open destroyed the data before
the lazy read could happen.

Reproduced with, e.g.:
  ./bin/prism -importmodel lec9ctl1.all -exportmodel lec9ctl1.all
(prism-tests/functionality/import/lec9ctl1*)
and similarly for lec3.all and irobot.all.
@davexparker
Add zip (gzip/xz) support for model export files.
f3a9cde 
Compresses exported files in place after writing, for both the explicit
and symbolic engines. Zipping can either be requested explicitly
(e.g. -exportmodel model.tra:zip=true) or automatically via a recognised
filename extension (e.g. -exportmodel model.tra.gz), which also works
with .all and the individual -export* switches.
@davexparker
Add transparent import of zipped explicit model files.
2f71fa8 
Detected from filename extension (.gz/.gzip/.xz), e.g.,
model.tra.gz or model.pexp.gz, when using -importmodel or
other related -importxx switches.

Plus regression tests.
@davexparker
Add "Whole model" (.pexp) export to "Model | Export | Plain text" GUI…
8202f34 
… menu.

Make sure existing transition export (.tra, Matlab) does indeed only
export transitions, not the whole model.
@davexparker
Small bug fixes in GUI export menus/dialogs.
02ec64f
@davexparker
Tidy up / deprecate some symbolic model export functions.
aadb463 
Also ensure that -exportprodtrans, -exportprodstates, -exportarget
are correctly using new code (and exporting headers by default).
@davexparker
Improve error messages for explicit model import parse failures.
69f028b 
Line numbers reported in parse errors were relative to the section
being read, not the underlying file (for comined .pexp).

Also fix extractVarInfoFromFile() dropping the underlying exception.
@davexparker
Support embedding properties-file labels in whole-model export (.pexp…
4e95ceb 
…/.drn/.umb).

Previously, "proplabels" only worked for standalone .lab exports
(-exportlabels/-exportproplabels); -exportmodel out.pexp:proplabels
silently ignored the flag, since combined-format exports never went
through a LABELS-entity ModelExportTask. Now it is always respected.
@davexparker
Bug fix in .tra file export.
67edb12
@davexparker
Explicit model import should set Model.varList from state info.
853347c
@davexparker davexparker requested a review from Copilot July 14, 2026 08:18
Copilot AI reviewed Jul 14, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This pull request improves PRISM model export/import by adding a combined explicit “whole model” format (.pexp), introducing consistent optional headers across explicit exports, and supporting zipped explicit-file workflows. It also fixes an MDP transition-rewards export bug by using per-state choice counts during iteration.

Changes:

  • Add combined explicit export/import (.pexp) that concatenates transitions, states, labels, observations, and rewards into one file (with mandatory section headers).
  • Add optional header emission + “append-to-file” plumbing across symbolic/explicit engines and the native exporters to support multi-section exports.
  • Add filename-extension–based compression support for import/export (.gz/.gzip/.xz) and update CLI/GUI + regression fixtures accordingly.

Reviewed changes

Copilot reviewed 176 out of 182 changed files in this pull request and generated 3 comments.

Show a summary per file
File Description
prism/unit-tests/io/PrismExplicitExporterTest.java New regression test for per-state choice counting in transition-rewards export.
prism/src/userinterface/model/GUIMultiModel.java Add “Whole model” export and ensure transition-only exports are explicit.
prism/src/symbolic/model/ProbModel.java Update export APIs to use ModelExportOptions, append, and headers.
prism/src/symbolic/model/NondetModel.java Update export APIs to use ModelExportOptions, append, and headers.
prism/src/symbolic/model/ModelSymbolic.java Add reward header builder; update states export to use ModelExportOptions.
prism/src/symbolic/model/Model.java Deprecate legacy export methods; route through ModelExportOptions.
prism/src/symbolic/comp/StateModelChecker.java Append multi-entity sections for .pexp; add zip support and header enforcement.
prism/src/symbolic/comp/ProbModelChecker.java Update product-state export to new states export API / label export signature.
prism/src/symbolic/comp/NondetModelChecker.java Update product-state export to new states export API / label export signature.
prism/src/symbolic/comp/MultiObjModelChecker.java Update label export signature with append/header parameters.
prism/src/sparse/PS_ExportSubMDP.cc Add append + header text support in native sparse exporter.
prism/src/sparse/PS_ExportMDP.cc Add append + header text support in native sparse exporter.
prism/src/sparse/PS_ExportMC.cc Add append + header text support in native sparse exporter.
prism/src/sparse/PS_ExportMatrix.cc Add append + header text support in native sparse exporter.
prism/src/sparse/PrismSparse.java Update JNI signatures and Java wrappers for append + header text.
prism/src/prism/PrismNative.cc Support appending exports by opening files with “a” mode.
prism/src/prism/PrismCL.java Add .pexp and zip-extension handling in import/export CLI flows.
prism/src/prism/Prism.java Plumb properties file into model checkers for export-time extra labels.
prism/src/mtbdd/PrismMTBDD.java Update JNI signatures and Java wrappers for append + header text.
prism/src/mtbdd/PM_ExportVector.cc Add append + header text support in native MTBDD exporter.
prism/src/mtbdd/PM_ExportMatrix.cc Add append + header text support in native MTBDD exporter.
prism/src/mtbdd/PM_ExportLabels.cc Add append + header text support in native MTBDD exporter.
prism/src/io/UMBExporter.java Skip deadlock AP in UMB if empty; minor label-export tweak.
prism/src/io/PrismExplicitImporter.java Add .pexp section parsing + zipped reading + header validation helpers.
prism/src/io/PrismExplicitExporter.java Add combined .pexp export mode + explicit headers; fix per-state choice iteration.
prism/src/io/ModelImportUnzipper.java New utility to transparently read compressed explicit import files.
prism/src/io/ModelExportZipper.java New utility to compress exported files post-write, with append-aware behavior.
prism/src/io/ModelExportTask.java Add .pexp handling, transition-only .tra behavior, and zip-extension retention.
prism/src/io/ModelExportOptions.java Add append-to-file option, transitions-only helper, and extension→compression mapping.
prism/src/explicit/StateModelChecker.java Add zip support + extra label merging; adjust label inclusion for explicit exports.
prism/src/explicit/ExplicitFiles2Model.java Ensure var list is set when loading explicit states.
prism/include/PrismNativeGlob.h Update native export-info API to accept append flag.
prism/include/jni/sparse_PrismSparse.h Update sparse JNI headers for new append/header parameters.
prism/include/jni/mtbdd_PrismMTBDD.h Update MTBDD JNI headers for new append/header parameters.
prism-tests/functionality/language/system.sm.tra Add explicit header line to fixture.
prism-tests/functionality/language/system.sm.sta Add explicit header line to fixture.
prism-tests/functionality/language/imdp-sync.tra Add explicit header line to fixture.
prism-tests/functionality/import/robot.tra Add explicit header line to fixture.
prism-tests/functionality/import/robot.sta Add explicit header line to fixture.
prism-tests/functionality/import/robot.pexp New combined explicit fixture.
prism-tests/functionality/import/robot.lab Add explicit header line to fixture.
prism-tests/functionality/import/poll2.tra Add explicit header line to fixture.
prism-tests/functionality/import/poll2.sta Add explicit header line to fixture.
prism-tests/functionality/import/poll2.pexp New combined explicit fixture.
prism-tests/functionality/import/poll2.lab Add explicit header line to fixture.
prism-tests/functionality/import/pexp.importexport.auto New regression script for .pexp round-trips and cross-format conversions.
prism-tests/functionality/import/mdp-deadlocks-fixed.tra Add explicit header line to fixture.
prism-tests/functionality/import/mdp-deadlocks-fixed.lab Add explicit header line to fixture.
prism-tests/functionality/import/mdp_simple.tra Add explicit header line to fixture.
prism-tests/functionality/import/mdp_simple.sta Add explicit header line to fixture.
prism-tests/functionality/import/mdp_simple.lab Add explicit header line to fixture.
prism-tests/functionality/import/maze.tra Add explicit header line to fixture.
prism-tests/functionality/import/maze.sta Add explicit header line to fixture.
prism-tests/functionality/import/maze.pexp New combined explicit fixture.
prism-tests/functionality/import/maze.obs Add explicit header line to fixture.
prism-tests/functionality/import/maze.lab Add explicit header line to fixture.
prism-tests/functionality/import/lec9ctl1.tra Add explicit header line to fixture.
prism-tests/functionality/import/lec9ctl1.sta Add explicit header line to fixture.
prism-tests/functionality/import/lec9ctl1.pexp New combined explicit fixture.
prism-tests/functionality/import/lec9ctl1.lab Add explicit header line to fixture.
prism-tests/functionality/import/lec3.tra Add explicit header line to fixture.
prism-tests/functionality/import/lec3.sta Add explicit header line to fixture.
prism-tests/functionality/import/lec3.pexp New combined explicit fixture.
prism-tests/functionality/import/lec3.lab Add explicit header line to fixture.
prism-tests/functionality/import/irobot.tra Add explicit header line to fixture.
prism-tests/functionality/import/irobot.sta Add explicit header line to fixture.
prism-tests/functionality/import/irobot.pexp New combined explicit fixture.
prism-tests/functionality/import/irobot.lab Add explicit header line to fixture.
prism-tests/functionality/import/dtmc-deadlocks-fixed.tra Add explicit header line to fixture.
prism-tests/functionality/import/dtmc-deadlocks-fixed.lab Add explicit header line to fixture.
prism-tests/functionality/import/dice2.tra Add explicit header line to fixture.
prism-tests/functionality/import/dice2.sta Add explicit header line to fixture.
prism-tests/functionality/import/dice2.lab Add explicit header line to fixture.
prism-tests/functionality/import/dice.tra Add explicit header line to fixture.
prism-tests/functionality/import/dice.sta Add explicit header line to fixture.
prism-tests/functionality/import/dice.pm.importzip.auto New regression script for zipped explicit imports.
prism-tests/functionality/import/dice.pexp New combined explicit fixture.
prism-tests/functionality/import/dice.lab Add explicit header line to fixture.
prism-tests/functionality/import/dice.exact.tra Add explicit header line to fixture.
prism-tests/functionality/import/dice.exact.sta Add explicit header line to fixture.
prism-tests/functionality/import/dice.exact.pexp New combined explicit exact-arithmetic fixture.
prism-tests/functionality/import/dice.exact.lab Add explicit header line to fixture.
prism-tests/functionality/import/dice-deadlock.tra Add explicit header line to fixture.
prism-tests/functionality/import/dice-deadlock.pexp New combined explicit deadlock fixture.
prism-tests/functionality/import/dice-deadlock.lab Add explicit header line to fixture.
prism-tests/functionality/import/badge.pepa.tra Add explicit header line to fixture.
prism-tests/functionality/import/badge.pepa.sta Add explicit header line to fixture.
prism-tests/functionality/import/badge.pepa.lab Add explicit header line to fixture.
prism-tests/functionality/export/target/robot.pm.reach.lab Add explicit header line to fixture.
prism-tests/functionality/export/target/robot.pm.ltl2.lab Add explicit header line to fixture.
prism-tests/functionality/export/target/robot.pm.ltl.lab Add explicit header line to fixture.
prism-tests/functionality/export/target/dice.pm.reach.lab Add explicit header line to fixture.
prism-tests/functionality/export/target/dice.pm.ltl.lab Add explicit header line to fixture.
prism-tests/functionality/export/pomdp/maze.prism.tra Add explicit header line to fixture.
prism-tests/functionality/export/pomdp/maze.prism.sta Add explicit header line to fixture.
prism-tests/functionality/export/pomdp/maze.prism.pexp New combined explicit export fixture.
prism-tests/functionality/export/pomdp/maze.prism.obs Add explicit header line to fixture.
prism-tests/functionality/export/pomdp/maze.prism.lab Add explicit header line to fixture.
prism-tests/functionality/export/pomdp/maze.prism.exportmodel.auto Add .pexp export to regression.
prism-tests/functionality/export/pomdp/import-pexp.auto New regression for .pexp import/export round-trip (POMDP).
prism-tests/functionality/export/mdp/robot.prism.tra Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.sta Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.rows.sta Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.rows.lab Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.pexp New combined explicit export fixture.
prism-tests/functionality/export/mdp/robot.prism.matlab.sta Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.lab Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.exportmodel.auto Add .pexp export cases (incl. exact).
prism-tests/functionality/export/mdp/robot.prism.exact.tra Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.exact.sta Add explicit header line to fixture.
prism-tests/functionality/export/mdp/robot.prism.exact.pexp New combined explicit exact-arithmetic export fixture.
prism-tests/functionality/export/mdp/robot.prism.exact.lab Add explicit header line to fixture.
prism-tests/functionality/export/mdp/import-pexp.auto New regression for .pexp import/export round-trip (MDP).
prism-tests/functionality/export/lts/lec9ctl1.prism.tra Add explicit header line to fixture.
prism-tests/functionality/export/lts/lec9ctl1.prism.sta Add explicit header line to fixture.
prism-tests/functionality/export/lts/lec9ctl1.prism.pexp New combined explicit export fixture.
prism-tests/functionality/export/lts/lec9ctl1.prism.lab Add explicit header line to fixture.
prism-tests/functionality/export/lts/lec9ctl1.prism.exportmodel.auto Add .pexp export to regression.
prism-tests/functionality/export/lts/import-pexp.auto New regression for .pexp import/export round-trip (LTS).
prism-tests/functionality/export/imdp/robot.prism.tra Add explicit header line to fixture.
prism-tests/functionality/export/imdp/robot.prism.sta Add explicit header line to fixture.
prism-tests/functionality/export/imdp/robot.prism.pexp New combined explicit export fixture.
prism-tests/functionality/export/imdp/robot.prism.lab Add explicit header line to fixture.
prism-tests/functionality/export/imdp/robot.prism.exportmodel.auto Add .pexp export to regression.
prism-tests/functionality/export/imdp/import-pexp.auto New regression for .pexp import/export round-trip (IMDP).
prism-tests/functionality/export/idtmc/import-pexp.auto New regression for .pexp import/export round-trip (IDTMC).
prism-tests/functionality/export/idtmc/dtmc_pctl.prism.tra Add explicit header line to fixture.
prism-tests/functionality/export/idtmc/dtmc_pctl.prism.sta Add explicit header line to fixture.
prism-tests/functionality/export/idtmc/dtmc_pctl.prism.pexp New combined explicit export fixture.
prism-tests/functionality/export/idtmc/dtmc_pctl.prism.lab Add explicit header line to fixture.
prism-tests/functionality/export/idtmc/dtmc_pctl.prism.exportmodel.auto Add .pexp export to regression.
prism-tests/functionality/export/dtmc/lec3.pm.tra Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/lec3.pm.sta Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/lec3.pm.pexp New combined explicit export fixture.
prism-tests/functionality/export/dtmc/lec3.pm.lab Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/lec3.pm.exportmodel.auto Add .pexp export cases to regression.
prism-tests/functionality/export/dtmc/import-pexp.auto New regression for .pexp import/export round-trip (DTMC).
prism-tests/functionality/export/dtmc/dice.pm.tra Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.sta Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.rows.sta Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.rows.lab Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.pexp New combined explicit export fixture.
prism-tests/functionality/export/dtmc/dice.pm.matlab.sta Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.labels2.props.args Add .pexp proplabels export regression entry.
prism-tests/functionality/export/dtmc/dice.pm.lab Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.exportmodel.auto Add .pexp export cases (incl. exact).
prism-tests/functionality/export/dtmc/dice.pm.exact.tra Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.exact.sta Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.exact.pexp New combined explicit exact-arithmetic export fixture.
prism-tests/functionality/export/dtmc/dice.pm.exact.lab Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.3.lab Add explicit header line to fixture.
prism-tests/functionality/export/dtmc/dice.pm.2.pexp New combined explicit export fixture (extra labels).
prism-tests/functionality/export/dtmc/dice.pm.2.lab Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/import-pexp.auto New regression for .pexp import/export round-trip (CTMC).
prism-tests/functionality/export/ctmc/cluster.sm.tra Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.sta Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.rows.sta Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.rows.lab Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.matlab.sta Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.lab Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.exportmodel.auto Add .pexp export cases (incl. exact).
prism-tests/functionality/export/ctmc/cluster.sm.exact.tra Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.exact.sta Add explicit header line to fixture.
prism-tests/functionality/export/ctmc/cluster.sm.exact.lab Add explicit header line to fixture.
prism-tests/bugfixes/trafileinit.tra Add explicit header line to fixture.
prism-tests/bugfixes/trafileinit.lab Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.pm.tra Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.pm.sta Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.pm.lab Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.nm.tra Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.nm.sta Add explicit header line to fixture.
prism-tests/bugfixes/export-precision/rare.nm.lab Add explicit header line to fixture.
prism-tests/bugfixes/advgenexplicit2.nm.props.adv.tra Add explicit header line to fixture.
prism-tests/bugfixes/advgenexplicit.nm.props.adv.tra Add explicit header line to fixture.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread prism/src/io/PrismExplicitImporter.java
Comment on lines +222 to +226
public int read(char[] cbuf, int off, int len) throws IOException
{
if (eof) {
return -1;
}
Comment thread prism/src/io/PrismExplicitImporter.java
Comment on lines +1953 to +1956
private static boolean isHeaderLike(String line)
{
return line.matches("# [A-Za-z()]+ *");
}
Comment thread prism/src/io/ModelImportUnzipper.java
Comment on lines +64 to +70
InputStream in = new BufferedInputStream(new FileInputStream(file));
try {
CompressorInputStream zipIn = new CompressorStreamFactory().createCompressorInputStream(zipFormat.get().extension(), in);
return new BufferedReader(new InputStreamReader(zipIn));
} catch (CompressorException e) {
throw new IOException("Could not read zipped file \"" + file + "\": " + e.getMessage());
}
@davexparker
Make PrismExplicitExporterTest robust to platform line endings.
331ef07 
(was failing Windows CI)
@davexparker
Fix LineBoundedReader.read() to honour the zero-length-read contract.
58b2f6d 
When called with len == 0, the loop condition (written < len) is
immediately false, so written stays 0 and the method returned -1
(EOF) instead of 0, per the java.io.Reader contract. A caller reading
in a loop and passing an empty buffer/length would incorrectly treat
this as end-of-stream.
@davexparker
Recognise multi-word headers in PrismExplicitImporter.isHeaderLike().
0013d5c
@davexparker
Close input stream on CompressorException in ModelImportUnzipper.
d4a2c64 
openBuffered() left the underlying (Buffered)FileInputStream open
when CompressorStreamFactory.createCompressorInputStream() failed
with a CompressorException, leaking the file handle before the
wrapped IOException was thrown.
@davexparker davexparker merged commit d4a2c64 into prismmodelchecker:master Jul 14, 2026
6 checks passed
@davexparker davexparker deleted the export+import branch July 14, 2026 18:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@davexparker