Skip to content

Commit 1cba8af

Browse files
committed
add CLI membership oracles
closes #149
1 parent 2345eea commit 1cba8af

File tree

13 files changed

+897
-0
lines changed

13 files changed

+897
-0
lines changed

oracles/membership-oracles/pom.xml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ limitations under the License.
5151
<groupId>org.checkerframework</groupId>
5252
<artifactId>checker-qual</artifactId>
5353
</dependency>
54+
<dependency>
55+
<groupId>org.slf4j</groupId>
56+
<artifactId>slf4j-api</artifactId>
57+
</dependency>
5458

5559
<!-- build -->
5660
<dependency>
Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.oracle.membership;
17+
18+
import java.io.IOException;
19+
import java.util.List;
20+
import java.util.Objects;
21+
22+
import de.learnlib.oracle.SingleQueryOracle;
23+
import net.automatalib.common.util.process.ProcessUtil;
24+
import net.automatalib.word.Word;
25+
import org.checkerframework.checker.nullness.qual.Nullable;
26+
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
27+
import org.slf4j.Logger;
28+
import org.slf4j.LoggerFactory;
29+
30+
/**
31+
* An oracle that delegates its queries to an external program via the command-line interface. Acceptance of the queries
32+
* is determined based on the program's return code where {@code 0} indicates success and any other value indicates
33+
* failure.
34+
* <p>
35+
* Queries are translated to program arguments (via the symbol's {@link #toString()} method). Depending on whether a
36+
* {@code reset} symbol has been specified, this oracle assumes either a stateless ({@code reset == null}) or stateful
37+
* ({@code reset != null}) communication.
38+
* <p>
39+
* In a stateless communication, all symbols of a query are passed to the program at once and invocations should be
40+
* treated independently from each other. In a stateful communication, the program is executed multiple times with a
41+
* single query symbol each, preceded by a single invocation with only the {@code reset} symbol. The exit code of the
42+
* last invocation determines the query response.
43+
*
44+
* @param <I>
45+
* input symbol type
46+
*/
47+
public class CLIOracle<I> implements SingleQueryOracle<I, Boolean> {
48+
49+
private static final Logger LOGGER = LoggerFactory.getLogger(CLIOracle.class);
50+
51+
private final List<String> commandLine;
52+
private final @Nullable String reset;
53+
54+
/**
55+
* Constructor. Does not set a {@code reset} symbol.
56+
*
57+
* @param commandLine
58+
* the command line, containing the main binary and potential additional arguments
59+
*
60+
* @see #CLIOracle(List, String)
61+
*/
62+
public CLIOracle(List<String> commandLine) {
63+
this(commandLine, null);
64+
}
65+
66+
/**
67+
* Constructor.
68+
*
69+
* @param commandLine
70+
* the command line, containing the main binary and potential additional arguments
71+
* @param reset
72+
* the symbol passed to the program to indicate a reset
73+
*/
74+
public CLIOracle(List<String> commandLine, @Nullable String reset) {
75+
this.commandLine = commandLine;
76+
this.reset = reset;
77+
}
78+
79+
@Override
80+
public Boolean answerQuery(Word<I> prefix, Word<I> suffix) {
81+
return reset == null ? answerStatelessQuery(prefix, suffix) : answerStatefulQuery(prefix, suffix);
82+
}
83+
84+
@SuppressWarnings("toarray.nullable.elements") // we make sure fo fill the remaining elements with non-null values
85+
private boolean answerStatelessQuery(Word<I> prefix, Word<I> suffix) {
86+
final String[] args = new String[this.commandLine.size() + prefix.size() + suffix.size()];
87+
int idx = this.commandLine.size();
88+
89+
this.commandLine.toArray(args);
90+
91+
for (I p : prefix) {
92+
args[idx++] = Objects.toString(p);
93+
}
94+
95+
for (I s : suffix) {
96+
args[idx++] = Objects.toString(s);
97+
}
98+
99+
try {
100+
return ProcessUtil.invokeProcess(args, LOGGER::debug, LOGGER::warn) == 0;
101+
} catch (IOException | InterruptedException e) {
102+
LOGGER.warn("Error while invoking process", e);
103+
return false;
104+
}
105+
}
106+
107+
@RequiresNonNull("this.reset")
108+
private boolean answerStatefulQuery(Word<I> prefix, Word<I> suffix) {
109+
try {
110+
int returnCode = ProcessUtil.invokeProcess(toCommand(commandLine, reset), LOGGER::debug, LOGGER::warn);
111+
112+
for (I p : prefix) {
113+
returnCode = ProcessUtil.invokeProcess(toCommand(commandLine, p), LOGGER::debug, LOGGER::warn);
114+
}
115+
116+
for (I s : suffix) {
117+
returnCode = ProcessUtil.invokeProcess(toCommand(commandLine, s), LOGGER::debug, LOGGER::warn);
118+
}
119+
120+
return returnCode == 0;
121+
} catch (IOException | InterruptedException e) {
122+
LOGGER.warn("Error while invoking process", e);
123+
return false;
124+
}
125+
}
126+
127+
@SuppressWarnings("toarray.nullable.elements") // we make sure fo fill the remaining elements with non-null values
128+
static <T> String[] toCommand(List<String> args, T arg) {
129+
final String[] result = new String[args.size() + 1];
130+
131+
args.toArray(result);
132+
result[args.size()] = Objects.toString(arg);
133+
134+
return result;
135+
}
136+
}
Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
/* Copyright (C) 2013-2025 TU Dortmund University
2+
* This file is part of LearnLib <https://learnlib.de>.
3+
*
4+
* Licensed under the Apache License, Version 2.0 (the "License");
5+
* you may not use this file except in compliance with the License.
6+
* You may obtain a copy of the License at
7+
*
8+
* http://www.apache.org/licenses/LICENSE-2.0
9+
*
10+
* Unless required by applicable law or agreed to in writing, software
11+
* distributed under the License is distributed on an "AS IS" BASIS,
12+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
* See the License for the specific language governing permissions and
14+
* limitations under the License.
15+
*/
16+
package de.learnlib.oracle.membership;
17+
18+
import java.io.IOException;
19+
import java.util.List;
20+
import java.util.Objects;
21+
import java.util.StringJoiner;
22+
import java.util.function.BiFunction;
23+
24+
import de.learnlib.oracle.SingleQueryOracle;
25+
import net.automatalib.common.util.process.ProcessUtil;
26+
import net.automatalib.word.Word;
27+
import org.checkerframework.checker.nullness.qual.Nullable;
28+
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
29+
import org.slf4j.Logger;
30+
import org.slf4j.LoggerFactory;
31+
32+
/**
33+
* An oracle that delegates its queries to an external program via the command-line interface. Outputs of the queries
34+
* are determined based on the provided output transformer.
35+
* <p>
36+
* Queries are translated to program arguments (via the symbol's {@link #toString()} method). Depending on whether a
37+
* {@code reset} symbol has been specified, this oracle assumes either a stateless ({@code reset == null}) or stateful
38+
* ({@code reset != null}) communication.
39+
* <p>
40+
* In a stateless communication, all symbols of a query are passed to the program at once and invocations should be
41+
* treated independently from each other. In a stateful communication, the program is executed multiple times with a
42+
* single query symbol each, preceded by a single invocation with only the {@code reset} symbol.
43+
*
44+
* @param <I>
45+
* input symbol type
46+
* @param <D>
47+
* output domain type
48+
*/
49+
public class CLIOutputOracle<I, D> implements SingleQueryOracle<I, D> {
50+
51+
private static final Logger LOGGER = LoggerFactory.getLogger(CLIOutputOracle.class);
52+
53+
private final List<String> commandLine;
54+
private final BiFunction<String, Integer, D> outputTransformer;
55+
private final @Nullable String reset;
56+
57+
/**
58+
* Constructor. Does not set a {@code reset} symbol.
59+
*
60+
* @param commandLine
61+
* the command line, containing the main binary and potential additional arguments
62+
* @param outputTransformer
63+
* the transformer for the program's output. Receives the full process output (stdin and stderr) as well as
64+
* the length of the query prefix for properly offsetting potentially {@link Word}-based output types.
65+
*
66+
* @see #CLIOutputOracle(List, BiFunction, String)
67+
*/
68+
public CLIOutputOracle(List<String> commandLine, BiFunction<String, Integer, D> outputTransformer) {
69+
this(commandLine, outputTransformer, null);
70+
}
71+
72+
/**
73+
* Constructor.
74+
*
75+
* @param commandLine
76+
* the command line, containing the main binary and potential additional arguments
77+
* @param outputTransformer
78+
* the transformer for the program's output. Receives the full process output (stdin and stderr) as well as
79+
* the length of the query prefix for properly offsetting potentially {@link Word}-based output types.
80+
* @param reset
81+
* the symbol passed to the program to indicate a reset
82+
*/
83+
public CLIOutputOracle(List<String> commandLine,
84+
BiFunction<String, Integer, D> outputTransformer,
85+
@Nullable String reset) {
86+
this.commandLine = commandLine;
87+
this.reset = reset;
88+
this.outputTransformer = outputTransformer;
89+
}
90+
91+
@Override
92+
public D answerQuery(Word<I> prefix, Word<I> suffix) {
93+
return reset == null ? answerStatelessQuery(prefix, suffix) : answerStatefulQuery(prefix, suffix);
94+
}
95+
96+
@SuppressWarnings("toarray.nullable.elements") // we make sure fo fill the remaining elements with non-null values
97+
private D answerStatelessQuery(Word<I> prefix, Word<I> suffix) {
98+
final String[] args = new String[this.commandLine.size() + prefix.size() + suffix.size()];
99+
int idx = this.commandLine.size();
100+
101+
this.commandLine.toArray(args);
102+
103+
for (I p : prefix) {
104+
args[idx++] = Objects.toString(p);
105+
}
106+
107+
for (I s : suffix) {
108+
args[idx++] = Objects.toString(s);
109+
}
110+
111+
final StringJoiner sj = new StringJoiner(System.lineSeparator());
112+
113+
try {
114+
ProcessUtil.invokeProcess(args, sj::add, LOGGER::warn);
115+
return outputTransformer.apply(sj.toString(), prefix.length());
116+
} catch (IOException | InterruptedException e) {
117+
throw new IllegalStateException(e);
118+
}
119+
}
120+
121+
@RequiresNonNull("this.reset")
122+
private D answerStatefulQuery(Word<I> prefix, Word<I> suffix) {
123+
final StringJoiner sj = new StringJoiner(System.lineSeparator());
124+
125+
try {
126+
ProcessUtil.invokeProcess(CLIOracle.toCommand(commandLine, reset), LOGGER::debug, LOGGER::warn);
127+
128+
for (I p : prefix) {
129+
ProcessUtil.invokeProcess(CLIOracle.toCommand(commandLine, p), sj::add, LOGGER::warn);
130+
}
131+
132+
for (I s : suffix) {
133+
ProcessUtil.invokeProcess(CLIOracle.toCommand(commandLine, s), sj::add, LOGGER::warn);
134+
}
135+
136+
return outputTransformer.apply(sj.toString(), prefix.length());
137+
} catch (IOException | InterruptedException e) {
138+
throw new IllegalStateException(e);
139+
}
140+
}
141+
}

0 commit comments

Comments
 (0)