Skip to content

Commit 17806bd

Browse files
davexparkerdavexparker
committed
Components using native code trigger use of native code for log writing.
PrismFileLog now defaults to using non-native code, i.e., PrintStreams, but can be switched cleanly to a native implementation using useNative(). Code using native libraries (mainly symbolic engines) implement new interface PrismNativeComponent, which triggers the switch on creation.
1 parent 117f52b commit 17806bd

11 files changed

Lines changed: 129 additions & 129 deletions

‎prism/src/jdd/JDDLibrary.java‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,13 @@ public void initialise(Prism prism) throws PrismException
4747
@Override
4848
public void setMainLog(PrismLog mainLog) throws PrismException
4949
{
50-
// If possible, pass the (file/stdout) pointer to JDD.
50+
// If possible, we ensure that the log is using native code
51+
// and pass the (file/stdout) pointer to JDD.
5152
// This is mainly so that diagnostic/error messages from the
5253
// DD native code end up in the same place as the rest of the log output.
54+
if (mainLog instanceof PrismFileLog) {
55+
((PrismFileLog) mainLog).useNative();
56+
}
5357
long fp = mainLog.getFilePointer();
5458
if (fp > 0) {
5559
JDD.SetOutputStream(fp);

‎prism/src/prism/PrismFileLog.java‎

Lines changed: 39 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,8 @@ public class PrismFileLog extends PrismPrintStreamLog
4040
protected String filename;
4141
/** Are we writing to stdout? */
4242
protected boolean stdout;
43+
/** Are we using native code to write to the file? */
44+
protected boolean nativeCode;
4345

4446
/**
4547
* Create a {@link PrismLog} which will write to {@code filename}, overwriting any previous contents.
@@ -61,7 +63,7 @@ public PrismFileLog(String filename) throws PrismException
6163
*/
6264
public PrismFileLog(String filename, boolean append) throws PrismException
6365
{
64-
this(filename, append, true);
66+
this(filename, append, false);
6567
}
6668

6769
/**
@@ -87,6 +89,7 @@ private void createLogStream(String filename, boolean append, boolean nativeCode
8789
{
8890
this.filename = filename;
8991
this.stdout = "stdout".equals(filename);
92+
this.nativeCode = nativeCode;
9093
try {
9194
if (nativeCode) {
9295
setPrintStream(new PrismFileLogNative(filename, append));
@@ -102,6 +105,20 @@ private void createLogStream(String filename, boolean append, boolean nativeCode
102105
}
103106
}
104107

108+
/**
109+
* Ensure the log is using native code to write to the file.
110+
* If this is currently not the case, this method will {@code close()}
111+
* the current log and open a new equivalent one using native code.
112+
* Throw a PRISM exception if there is a problem opening the file for writing.
113+
*/
114+
public void useNative() throws PrismException
115+
{
116+
if (!nativeCode) {
117+
close();
118+
createLogStream(filename, true, true);
119+
}
120+
}
121+
105122
/**
106123
* Get the filename (or "stdout" if writing to standard output)
107124
**/
@@ -110,6 +127,14 @@ public String getFileName()
110127
return stdout ? "stdout" : filename;
111128
}
112129

130+
/**
131+
* Is this log using native code to write to the file?
132+
*/
133+
public boolean isNative()
134+
{
135+
return nativeCode;
136+
}
137+
113138
// Methods for PrismLog
114139

115140
@Override
@@ -161,6 +186,19 @@ public static PrismFileLog create(String filename, boolean append) throws PrismE
161186
return new PrismFileLog(filename, append);
162187
}
163188

189+
/**
190+
* Create a {@link PrismLog} which will write to {@code filename}, appending to an existing file if requested.
191+
* If {@code filename} is "stdout", then output will be written to standard output.
192+
* Throw a PRISM exception if there is a problem opening the file for writing.
193+
* @param filename Filename of log file
194+
* @param append Append to the existing file?
195+
* @param nativeCode Use native code to write to the file?
196+
*/
197+
public static PrismFileLog create(String filename, boolean append, boolean nativeCode) throws PrismException
198+
{
199+
return new PrismFileLog(filename, append, nativeCode);
200+
}
201+
164202
/**
165203
* Create a {@link PrismLog} which will write to standard output.
166204
*/

‎prism/src/prism/PrismNativeComponent.java‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
//==============================================================================
2+
//
3+
// Copyright (c) 2026-
4+
// Authors:
5+
// * Dave Parker <david.parker@cs.ox.ac.uk> (University of Oxford)
6+
//
7+
//------------------------------------------------------------------------------
8+
//
9+
// This file is part of PRISM.
10+
//
11+
// PRISM is free software; you can redistribute it and/or modify
12+
// it under the terms of the GNU General Public License as published by
13+
// the Free Software Foundation; either version 2 of the License, or
14+
// (at your option) any later version.
15+
//
16+
// PRISM is distributed in the hope that it will be useful,
17+
// but WITHOUT ANY WARRANTY; without even the implied warranty of
18+
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19+
// GNU General Public License for more details.
20+
//
21+
// You should have received a copy of the GNU General Public License
22+
// along with PRISM; if not, write to the Free Software Foundation,
23+
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
24+
//
25+
//==============================================================================
26+
27+
package prism;
28+
29+
/**
30+
* Base class for {@link PrismComponent}s that use native code.
31+
*/
32+
public class PrismNativeComponent extends PrismComponent
33+
{
34+
/* Reference to the parent Prism instance. */
35+
protected Prism prism;
36+
37+
public PrismNativeComponent(Prism prism) throws PrismException
38+
{
39+
super(prism);
40+
this.prism = prism;
41+
}
42+
}

‎prism/src/symbolic/build/ExplicitFiles2MTBDD.java‎

Lines changed: 5 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -38,16 +38,7 @@
3838
import parser.Values;
3939
import parser.VarList;
4040
import parser.ast.DeclarationType;
41-
import prism.Evaluator;
42-
import prism.ModelInfo;
43-
import prism.ModelType;
44-
import prism.Prism;
45-
import prism.PrismException;
46-
import prism.PrismLog;
47-
import prism.PrismNotSupportedException;
48-
import prism.PrismSettings;
49-
import prism.ProgressDisplay;
50-
import prism.RewardInfo;
41+
import prism.*;
5142
import symbolic.model.Model;
5243
import symbolic.model.ModelSymbolic;
5344
import symbolic.model.ModelVariablesDD;
@@ -58,12 +49,8 @@
5849
/**
5950
* Class to convert explicit-state file storage of a model to symbolic representation.
6051
*/
61-
public class ExplicitFiles2MTBDD
52+
public class ExplicitFiles2MTBDD extends PrismNativeComponent
6253
{
63-
// Prism stuff
64-
private Prism prism;
65-
private PrismLog mainLog;
66-
6754
// Importer / files to read in from
6855
private ExplicitModelImporter importer;
6956

@@ -112,10 +99,9 @@ public class ExplicitFiles2MTBDD
11299
private ProgressDisplay progress;
113100
private int transitionsImported;
114101

115-
public ExplicitFiles2MTBDD(Prism prism)
102+
public ExplicitFiles2MTBDD(Prism prism) throws PrismException
116103
{
117-
this.prism = prism;
118-
mainLog = prism.getMainLog();
104+
super(prism);
119105
}
120106

121107
/**
@@ -290,7 +276,7 @@ private void allocateDDVars() throws PrismException
290276

291277
modelVariables = new ModelVariablesDD();
292278

293-
modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
279+
modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
294280

295281
// create arrays/etc. first
296282

‎prism/src/symbolic/build/ExplicitModel2MTBDD.java‎

Lines changed: 5 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -32,28 +32,16 @@
3232
import parser.*;
3333
import parser.ast.*;
3434
import explicit.*;
35-
import prism.ModelType;
36-
import prism.Prism;
37-
import prism.PrismException;
38-
import prism.PrismLangException;
39-
import prism.PrismLog;
40-
import prism.PrismSettings;
41-
import prism.ProgressDisplay;
35+
import prism.*;
4236
import symbolic.model.ModelVariablesDD;
4337
import symbolic.model.ProbModel;
4438
import symbolic.model.StochModel;
4539

4640
/**
4741
* Class to convert explicit-state representation of a model to a symbolic one.
4842
*/
49-
public class ExplicitModel2MTBDD
43+
public class ExplicitModel2MTBDD extends PrismNativeComponent
5044
{
51-
// prism
52-
private Prism prism;
53-
54-
// logs
55-
private PrismLog mainLog; // main log
56-
5745
// Explicit-state model
5846
private explicit.Model<Double> modelExpl;
5947

@@ -96,10 +84,9 @@ public class ExplicitModel2MTBDD
9684

9785
// constructor
9886

99-
public ExplicitModel2MTBDD(Prism prism)
87+
public ExplicitModel2MTBDD(Prism prism) throws PrismException
10088
{
101-
this.prism = prism;
102-
mainLog = prism.getMainLog();
89+
super(prism);
10390
}
10491

10592
// Build model
@@ -249,7 +236,7 @@ private void allocateDDVars()
249236

250237
modelVariables = new ModelVariablesDD();
251238

252-
modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
239+
modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
253240

254241
// create arrays/etc. first
255242

‎prism/src/symbolic/build/ModelGenerator2MTBDD.java‎

Lines changed: 5 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -38,15 +38,7 @@
3838
import parser.ast.DeclarationClock;
3939
import parser.ast.DeclarationIntUnbounded;
4040
import parser.ast.DeclarationType;
41-
import prism.ModelGenerator;
42-
import prism.ModelType;
43-
import prism.Prism;
44-
import prism.PrismException;
45-
import prism.PrismLangException;
46-
import prism.PrismLog;
47-
import prism.PrismNotSupportedException;
48-
import prism.PrismSettings;
49-
import prism.RewardGenerator;
41+
import prism.*;
5042
import symbolic.model.Model;
5143
import symbolic.model.ModelSymbolic;
5244
import symbolic.model.ModelVariablesDD;
@@ -57,12 +49,8 @@
5749
/**
5850
* Class to construct a symbolic representation from a ModelGenerator object.
5951
*/
60-
public class ModelGenerator2MTBDD
52+
public class ModelGenerator2MTBDD extends PrismNativeComponent
6153
{
62-
// Prism stuff
63-
private Prism prism;
64-
private PrismLog mainLog;
65-
6654
// Source model generators
6755
private ModelGenerator<Double> modelGen;
6856
private RewardGenerator<Double> rewardGen;
@@ -102,10 +90,9 @@ public class ModelGenerator2MTBDD
10290

10391
private int maxNumChoices = 0;
10492

105-
public ModelGenerator2MTBDD(Prism prism)
93+
public ModelGenerator2MTBDD(Prism prism) throws PrismException
10694
{
107-
this.prism = prism;
108-
mainLog = prism.getMainLog();
95+
super(prism);
10996
}
11097

11198
/**
@@ -228,7 +215,7 @@ private void allocateDDVars() throws PrismException
228215
JDDNode vr, vc;
229216
int i, j, n;
230217

231-
modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
218+
modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
232219

233220
// create arrays/etc. first
234221

‎prism/src/symbolic/build/Modules2MTBDD.java‎

Lines changed: 8 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -45,17 +45,11 @@
4545

4646
// class to translate a modules description file into an MTBDD model
4747

48-
public class Modules2MTBDD
48+
public class Modules2MTBDD extends PrismNativeComponent
4949
{
50-
// Prism object
51-
private Prism prism;
52-
5350
// StateModelChecker for expression -> MTBDD conversion
5451
private StateModelChecker expr2mtbdd;
5552

56-
// logs
57-
private PrismLog mainLog; // main log
58-
5953
// ModulesFile object to store syntax tree from parser
6054
private ModulesFile modulesFile;
6155

@@ -232,13 +226,12 @@ public SystemDDs(int n)
232226

233227
// constructor
234228

235-
public Modules2MTBDD(Prism p, ModulesFile mf)
229+
public Modules2MTBDD(Prism prism, ModulesFile mf) throws PrismException
236230
{
237-
prism = p;
238-
mainLog = p.getMainLog();
231+
super(prism);
239232
modulesFile = mf;
240233
// get symmetry reduction info
241-
String s = prism.getSettings().getString(PrismSettings.PRISM_SYMM_RED_PARAMS);
234+
String s = settings.getString(PrismSettings.PRISM_SYMM_RED_PARAMS);
242235
doSymmetry = !(s == null || s == "");
243236
}
244237

@@ -482,7 +475,7 @@ private void allocateDDVars()
482475
case 1:
483476
// ordering: (a ... a) (s ... s) (l ... l) (r c ... r c)
484477

485-
modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
478+
modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
486479

487480
// create arrays/etc. first
488481

@@ -538,7 +531,7 @@ private void allocateDDVars()
538531
// create a gap in the dd variables
539532
// this allows to prepend additional row/col vars, e.g. for constructing
540533
// a product model when doing LTL model checking
541-
modelVariables.preallocateExtraStateVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_STATE_VARS));
534+
modelVariables.preallocateExtraStateVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_STATE_VARS));
542535

543536

544537
// allocate dd variables for module variables (i.e. rows/cols)
@@ -562,7 +555,7 @@ private void allocateDDVars()
562555
case 2:
563556
// ordering: (a ... a) (l ... l) (s r c ... r c) (s r c ... r c) ...
564557

565-
modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
558+
modelVariables.preallocateExtraActionVariables(settings.getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
566559

567560
// create arrays/etc. first
568561

@@ -2216,7 +2209,7 @@ private void doSymmetry(ModelSymbolic model) throws PrismException
22162209
String ss[];
22172210

22182211
// parse symmetry reduction parameters
2219-
ss = prism.getSettings().getString(PrismSettings.PRISM_SYMM_RED_PARAMS).split(" ");
2212+
ss = settings.getString(PrismSettings.PRISM_SYMM_RED_PARAMS).split(" ");
22202213
if (ss.length != 2) throw new PrismException ("Invalid parameters for symmetry reduction");
22212214
try {
22222215
numModulesBeforeSymm = Integer.parseInt(ss[0].trim());

0 commit comments

Comments
 (0)