Skip to content

Commit af66585

Browse files
agacekagacek
committed
Realizability checking based on work by Andreas Katis
1 parent eff1b4f commit af66585

File tree

106 files changed

+3295
-1252
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

106 files changed

+3295
-1252
lines changed

‎.gitattributes

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
.project text
77
.classpath text
88
*.userlibraries text
9-
.settings/* text
9+
*/.settings/* text
1010
*.jardesc text
1111
*.launch text
1212
LICENSE text

‎.gitignore

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
bin
2-
*.xml
3-
*.yc
4-
*.smt2
5-
*.xls
6-
*.log
7-
*.csv
1+
bin
2+
*.xml
3+
*.yc
4+
*.smt2
5+
*.xls
6+
*.log
7+
*.csv

‎jkind-api/src/jkind/api/ApiUtil.java

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
package jkind.api;
2+
3+
import java.io.BufferedInputStream;
4+
import java.io.File;
5+
import java.io.IOException;
6+
import java.io.InputStream;
7+
import java.util.function.Function;
8+
9+
import jkind.JKindException;
10+
import jkind.api.results.JKindResult;
11+
import jkind.api.xml.JKindXmlFileInputStream;
12+
import jkind.api.xml.XmlParseThread;
13+
import jkind.util.Util;
14+
15+
import org.eclipse.core.runtime.IProgressMonitor;
16+
17+
public class ApiUtil {
18+
public static File writeLustreFile(String program) {
19+
File file = null;
20+
try {
21+
file = File.createTempFile("jkind-api", ".lus");
22+
Util.writeToFile(program, file);
23+
return file;
24+
} catch (IOException e) {
25+
safeDelete(file);
26+
throw new JKindException("Cannot write to file: " + file, e);
27+
}
28+
}
29+
30+
public static void safeDelete(File file) {
31+
if (file != null && file.exists()) {
32+
file.delete();
33+
}
34+
}
35+
36+
public static void execute(Function<File, ProcessBuilder> runCommand, File lustreFile,
37+
JKindResult result, IProgressMonitor monitor) {
38+
File xmlFile = null;
39+
try {
40+
xmlFile = getXmlFile(lustreFile);
41+
ApiUtil.safeDelete(xmlFile);
42+
if (xmlFile.exists()) {
43+
throw new JKindException("Existing XML file cannot be removed: " + xmlFile);
44+
}
45+
callJKind(runCommand, lustreFile, xmlFile, result, monitor);
46+
} catch (JKindException e) {
47+
throw e;
48+
} catch (Throwable t) {
49+
throw new JKindException(result.getText(), t);
50+
} finally {
51+
ApiUtil.safeDelete(xmlFile);
52+
}
53+
}
54+
55+
private static File getXmlFile(File lustreFile) {
56+
return new File(lustreFile.toString() + ".xml");
57+
}
58+
59+
private static void callJKind(Function<File, ProcessBuilder> runCommand, File lustreFile,
60+
File xmlFile, JKindResult result, IProgressMonitor monitor) throws IOException,
61+
InterruptedException {
62+
ProcessBuilder builder = runCommand.apply(lustreFile);
63+
Process process = null;
64+
try (JKindXmlFileInputStream xmlStream = new JKindXmlFileInputStream(xmlFile)) {
65+
XmlParseThread parseThread = new XmlParseThread(xmlStream, result, Backend.JKIND);
66+
67+
try {
68+
result.start();
69+
process = builder.start();
70+
parseThread.start();
71+
result.setText(ApiUtil.readOutput(process, monitor));
72+
} finally {
73+
int code = 0;
74+
if (process != null) {
75+
process.destroy();
76+
code = process.waitFor();
77+
}
78+
79+
xmlStream.done();
80+
parseThread.join();
81+
82+
if (monitor.isCanceled()) {
83+
result.cancel();
84+
} else {
85+
result.done();
86+
}
87+
monitor.done();
88+
89+
if (code != 0 && !monitor.isCanceled()) {
90+
throw new JKindException("Abnormal termination, exit code " + code);
91+
}
92+
}
93+
94+
if (parseThread.getThrowable() != null) {
95+
throw new JKindException("Error parsing XML", parseThread.getThrowable());
96+
}
97+
}
98+
}
99+
100+
public static String readOutput(Process process, IProgressMonitor monitor) throws IOException {
101+
InputStream stream = new BufferedInputStream(process.getInputStream());
102+
StringBuilder text = new StringBuilder();
103+
104+
while (true) {
105+
if (monitor.isCanceled()) {
106+
return text.toString();
107+
} else if (stream.available() > 0) {
108+
int c = stream.read();
109+
if (c == -1) {
110+
return text.toString();
111+
}
112+
text.append((char) c);
113+
} else if (isTerminated(process)) {
114+
return text.toString();
115+
} else {
116+
try {
117+
Thread.sleep(100);
118+
} catch (InterruptedException e) {
119+
}
120+
}
121+
}
122+
}
123+
124+
public static boolean isTerminated(Process process) {
125+
try {
126+
process.exitValue();
127+
return true;
128+
} catch (IllegalThreadStateException e) {
129+
return false;
130+
}
131+
}
132+
133+
public static File findJKindJar() {
134+
/*
135+
* On Windows, invoking Process.destroy does not kill the subprocesses
136+
* of the destroyed process. If we were to run jkind.bat and kill it,
137+
* only the cmd.exe process which is running the batch file would be
138+
* killed. The underlying JKind process would continue to its natural
139+
* end. To avoid this, we search the user's path for the jkind.jar file
140+
* and invoke it directly.
141+
*
142+
* In order to support JKIND_HOME or PATH as the location for JKind, we
143+
* now search in non-windows environments too.
144+
*/
145+
146+
File jar = findJKindJar(System.getenv("JKIND_HOME"));
147+
if (jar != null) {
148+
return jar;
149+
}
150+
151+
jar = findJKindJar(System.getenv("PATH"));
152+
if (jar != null) {
153+
return jar;
154+
}
155+
156+
throw new JKindException("Unable to find jkind.jar in JKIND_HOME or on system PATH");
157+
}
158+
159+
public static File findJKindJar(String path) {
160+
if (path == null) {
161+
return null;
162+
}
163+
164+
for (String element : path.split(File.pathSeparator)) {
165+
File jar = new File(element, "jkind.jar");
166+
if (jar.exists()) {
167+
return jar;
168+
}
169+
}
170+
171+
return null;
172+
}
173+
174+
public static String readAll(InputStream inputStream) throws IOException {
175+
StringBuilder result = new StringBuilder();
176+
BufferedInputStream buffered = new BufferedInputStream(inputStream);
177+
int i;
178+
while ((i = buffered.read()) != -1) {
179+
result.append((char) i);
180+
}
181+
return result.toString();
182+
}
183+
}

‎jkind-api/src/jkind/api/JKindApi.java

Lines changed: 4 additions & 149 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,13 @@
11
package jkind.api;
22

3-
import java.io.BufferedInputStream;
43
import java.io.File;
5-
import java.io.IOException;
6-
import java.io.InputStream;
74
import java.util.ArrayList;
85
import java.util.Arrays;
96
import java.util.List;
107

118
import jkind.JKindException;
129
import jkind.SolverOption;
1310
import jkind.api.results.JKindResult;
14-
import jkind.api.xml.JKindXmlFileInputStream;
15-
import jkind.api.xml.XmlParseThread;
1611

1712
import org.eclipse.core.runtime.IProgressMonitor;
1813

@@ -120,94 +115,7 @@ public void setIntervalGeneralization() {
120115
*/
121116
@Override
122117
public void execute(File lustreFile, JKindResult result, IProgressMonitor monitor) {
123-
File xmlFile = null;
124-
try {
125-
xmlFile = getXmlFile(lustreFile);
126-
safeDelete(xmlFile);
127-
if (xmlFile.exists()) {
128-
throw new JKindException("Existing XML file cannot be removed: " + xmlFile);
129-
}
130-
callJKind(lustreFile, xmlFile, result, monitor);
131-
} catch (JKindException e) {
132-
throw e;
133-
} catch (Throwable t) {
134-
throw new JKindException(result.getText(), t);
135-
} finally {
136-
safeDelete(xmlFile);
137-
}
138-
}
139-
140-
private void callJKind(File lustreFile, File xmlFile, JKindResult result,
141-
IProgressMonitor monitor) throws IOException, InterruptedException {
142-
ProcessBuilder builder = getJKindProcessBuilder(lustreFile);
143-
Process process = null;
144-
try (JKindXmlFileInputStream xmlStream = new JKindXmlFileInputStream(xmlFile)) {
145-
XmlParseThread parseThread = new XmlParseThread(xmlStream, result, Backend.JKIND);
146-
147-
try {
148-
result.start();
149-
process = builder.start();
150-
parseThread.start();
151-
readOutput(process, result, monitor);
152-
} finally {
153-
int code = 0;
154-
if (process != null) {
155-
process.destroy();
156-
code = process.waitFor();
157-
}
158-
159-
xmlStream.done();
160-
parseThread.join();
161-
162-
if (monitor.isCanceled()) {
163-
result.cancel();
164-
} else {
165-
result.done();
166-
}
167-
monitor.done();
168-
169-
if (code != 0 && !monitor.isCanceled()) {
170-
throw new JKindException("Abnormal termination, exit code " + code);
171-
}
172-
}
173-
174-
if (parseThread.getThrowable() != null) {
175-
throw new JKindException("Error parsing XML", parseThread.getThrowable());
176-
}
177-
}
178-
}
179-
180-
private void readOutput(Process process, final JKindResult result, IProgressMonitor monitor)
181-
throws IOException {
182-
final InputStream stream = new BufferedInputStream(process.getInputStream());
183-
184-
while (true) {
185-
if (monitor.isCanceled()) {
186-
return;
187-
} else if (stream.available() > 0) {
188-
int c = stream.read();
189-
if (c == -1) {
190-
return;
191-
}
192-
result.addText((char) c);
193-
} else if (isTerminated(process)) {
194-
return;
195-
} else {
196-
try {
197-
Thread.sleep(100);
198-
} catch (InterruptedException e) {
199-
}
200-
}
201-
}
202-
}
203-
204-
private boolean isTerminated(Process process) {
205-
try {
206-
process.exitValue();
207-
return true;
208-
} catch (IllegalThreadStateException e) {
209-
return false;
210-
}
118+
ApiUtil.execute(this::getJKindProcessBuilder, lustreFile, result, monitor);
211119
}
212120

213121
private ProcessBuilder getJKindProcessBuilder(File lustreFile) {
@@ -259,51 +167,8 @@ private ProcessBuilder getJKindProcessBuilder(File lustreFile) {
259167
return builder;
260168
}
261169

262-
private String[] getJKindCommand() {
263-
/*
264-
* On Windows, invoking Process.destroy does not kill the subprocesses
265-
* of the destroyed process. If we were to run jkind.bat and kill it,
266-
* only the cmd.exe process which is running the batch file would be
267-
* killed. The underlying JKind process would continue to its natural
268-
* end. To avoid this, we search the user's path for the jkind.jar file
269-
* and invoke it directly.
270-
*
271-
* In order to support JKIND_HOME or PATH as the location for JKind, we
272-
* now search in non-windows environments too.
273-
*/
274-
275-
File jar = findJKindJar();
276-
if (jar == null) {
277-
throw new JKindException("Unable to find jkind.jar in JKIND_HOME or on system PATH");
278-
}
279-
return new String[] { "java", "-jar", jar.toString(), "-jkind" };
280-
}
281-
282-
private File findJKindJar() {
283-
File jar = findJKindJar(System.getenv("JKIND_HOME"));
284-
if (jar == null) {
285-
jar = findJKindJar(System.getenv("PATH"));
286-
}
287-
return jar;
288-
}
289-
290-
private File findJKindJar(String path) {
291-
if (path == null) {
292-
return null;
293-
}
294-
295-
for (String element : path.split(File.pathSeparator)) {
296-
File jar = new File(element, "jkind.jar");
297-
if (jar.exists()) {
298-
return jar;
299-
}
300-
}
301-
302-
return null;
303-
}
304-
305-
private static File getXmlFile(File lustreFile) {
306-
return new File(lustreFile.toString() + ".xml");
170+
private static String[] getJKindCommand() {
171+
return new String[] { "java", "-jar", ApiUtil.findJKindJar().toString(), "-jkind" };
307172
}
308173

309174
@Override
@@ -316,19 +181,9 @@ public void checkAvailable() throws Exception {
316181
builder.redirectErrorStream(true);
317182
Process process = builder.start();
318183

319-
String output = readAll(process.getInputStream());
184+
String output = ApiUtil.readAll(process.getInputStream());
320185
if (process.exitValue() != 0) {
321186
throw new JKindException("Error running JKind: " + output);
322187
}
323188
}
324-
325-
private String readAll(InputStream inputStream) throws IOException {
326-
StringBuilder result = new StringBuilder();
327-
BufferedInputStream buffered = new BufferedInputStream(inputStream);
328-
int i;
329-
while ((i = buffered.read()) != -1) {
330-
result.append((char) i);
331-
}
332-
return result.toString();
333-
}
334189
}

0 commit comments

Comments
 (0)