-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Testing if an input program is given; adding tests for the main entry…
… point of Alpha. - Adding test runs that previously triggered exceptions.
- Loading branch information
Showing
4 changed files
with
206 additions
and
55 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,69 +1,59 @@ | ||
package at.ac.tuwien.kr.alpha; | ||
|
||
import ch.qos.logback.classic.Level; | ||
import ch.qos.logback.classic.Logger; | ||
import org.junit.Ignore; | ||
import org.junit.Test; | ||
import org.slf4j.LoggerFactory; | ||
|
||
import java.io.ByteArrayInputStream; | ||
import java.io.IOException; | ||
import java.io.ByteArrayOutputStream; | ||
import java.io.InputStream; | ||
import java.io.PrintStream; | ||
|
||
import static at.ac.tuwien.kr.alpha.Main.main; | ||
import static at.ac.tuwien.kr.alpha.Main.parseVisit; | ||
import static org.junit.Assert.assertTrue; | ||
|
||
public class MainTest { | ||
public static InputStream stream(String file) { | ||
return new ByteArrayInputStream(file.getBytes()); | ||
} | ||
|
||
@Test | ||
@Ignore | ||
public void parseSimpleProgram() throws IOException { | ||
parseVisit( | ||
"p(X) :- q(X).\n" + | ||
"q(a).\n" + | ||
"q(b).\n" | ||
); | ||
/** | ||
* Temporarily redirects System.err and System.out while running the solver from the main entry point with the given parameters. | ||
* Returns true if the output contains the given matches. | ||
* Warning: this test is fragile and may require adaptions if printing is changed anywhere in Alpha. | ||
* @param argv the arguments the solver is started with. | ||
* @param matchOutput output that must occur on System.out - may be null if irrelevant. | ||
* @param matchError the output that must occur on System.err - may be null if irrelevant. | ||
* @return true if given output and errors appear on System.out and System.err while running main(argv). | ||
*/ | ||
private boolean testMainForOutput(String[] argv, String matchOutput, String matchError) { | ||
PrintStream oldErr = System.err; | ||
PrintStream oldOut = System.out; | ||
ByteArrayOutputStream newOut = new ByteArrayOutputStream(); | ||
ByteArrayOutputStream newErr = new ByteArrayOutputStream(); | ||
System.setOut(new PrintStream(newOut)); | ||
System.setErr(new PrintStream(newErr)); | ||
main(argv); | ||
System.setOut(oldOut); | ||
System.setErr(oldErr); | ||
|
||
return !(matchOutput != null && !newOut.toString().contains(matchOutput)) | ||
&& !(matchError != null && !newErr.toString().contains(matchError)); | ||
} | ||
|
||
@Test | ||
public void parseProgramWithNegativeBody() throws IOException { | ||
parseVisit( | ||
"p(X) :- q(X), not q(a).\n" + | ||
"q(a).\n" | ||
); | ||
} | ||
|
||
@Test(expected = UnsupportedOperationException.class) | ||
@Ignore | ||
public void parseProgramWithFunction() throws IOException { | ||
parseVisit( | ||
"p(X) :- q(f(X)).\n" + | ||
"q(a).\n" | ||
); | ||
} | ||
|
||
@Test(expected = UnsupportedOperationException.class) | ||
@Ignore | ||
public void parseProgramWithDisjunctionInHead() throws IOException { | ||
parseVisit( | ||
"r(X) | q(X) :- q(X).\n" + | ||
"q(a).\n" | ||
); | ||
public void testCommandLineOptions() { | ||
// Exercise the main entry point of the solver. | ||
assertTrue(testMainForOutput(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-e", "1119654162577372", "-n", "20", "-str", "p(a). \n b :- p(X).\n"}, "{ b(), p(a) }", null)); | ||
assertTrue(testMainForOutput(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-n", "0", "-str", "p(a). \n b :- p(X).\n"}, "{ b(), p(a) }", null)); | ||
assertTrue(testMainForOutput(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-n", "1", "-str", "p(a). \n b :- p(X).\n"}, "{ b(), p(a) }", null)); | ||
assertTrue(testMainForOutput(new String[]{"-g", "naive", "-s", "default", "-r", "naive", "-e", "1119654162577372", "-n", "1", "-str", "p(a). \n b :- p(X).\n"}, "{ b(), p(a) }", null)); | ||
} | ||
|
||
@Test | ||
@Ignore | ||
public void testLargeInputProgram() { | ||
Logger root = (Logger) LoggerFactory.getLogger(Logger.ROOT_LOGGER_NAME); | ||
root.setLevel(Level.DEBUG); | ||
//main(new String[]{"-g", "naive", "-s", "default", "-n", "2", "-i", "./benchmarks/omiga/omiga-testcases/locstrat/locstrat-200.txt"}); | ||
//main(new String[]{"-g", "naive", "-s", "default", "-n", "2", "-i", "./benchmarks/omiga/omiga-testcases/cutedge/cutedge-100-50.txt"}); | ||
//main(new String[]{"-g", "naive", "-s", "default", "-n", "10", "-i", "./benchmarks/omiga/omiga-testcases/3col/3col-20-38.txt"}); | ||
//main(new String[]{"-g", "naive", "-s", "naive", "-n", "10", "-i", "./benchmarks/omiga/omiga-testcases/reach/reach-1.txt"}); | ||
main(new String[]{"-g", "naive", "-s", "default", "-n", "1", "-i", "./benchmarks/siemens/vehicle_normal_small.asp"}); | ||
public void previouslyProblematicRuns() { | ||
// Run tests that formerly caused some sort of exception. | ||
main(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-e", "1119654162577372", "-n", "200", "-i", "./src/test/resources/PreviouslyProblematic/3col-20-38.txt"}); | ||
main(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-e", "1119718541727902", "-n", "200", "-i", ".//src/test/resources/PreviouslyProblematic/3col-20-38.txt"}); | ||
main(new String[]{"-DebugEnableInternalChecks", "-g", "naive", "-s", "default", "-e", "97598271567626", "-n", "2", "-i", "./src/test/resources/PreviouslyProblematic/vehicle_normal_small.asp"}); | ||
main(new String[]{"-DebugEnableInternalChecks", "-sort", "-g", "naive", "-s", "default", "-n", "400", "-i", "./src/test/resources/PreviouslyProblematic/3col-20-38.txt"}); | ||
} | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,67 @@ | ||
blue(N) :- node(N), not red(N), not green(N). | ||
red(N) :- node(N), not blue(N), not green(N). | ||
green(N) :- node(N), not red(N), not blue(N). | ||
|
||
:- link(N1,N2), blue(N1), blue(N2). | ||
:- link(N1,N2), red(N1), red(N2). | ||
:- link(N1,N2), green(N1), green(N2). | ||
|
||
node(0). | ||
node(1). | ||
node(2). | ||
node(3). | ||
node(4). | ||
node(5). | ||
node(6). | ||
node(7). | ||
node(8). | ||
node(9). | ||
node(10). | ||
node(11). | ||
node(12). | ||
node(13). | ||
node(14). | ||
node(15). | ||
node(17). | ||
node(16). | ||
node(19). | ||
node(18). | ||
link(5,10).link(10,5). | ||
link(4,5).link(5,4). | ||
link(5,9).link(9,5). | ||
link(6,12).link(12,6). | ||
link(4,13).link(13,4). | ||
link(10,19).link(19,10). | ||
link(4,7).link(7,4). | ||
link(6,13).link(13,6). | ||
link(0,13).link(13,0). | ||
link(9,15).link(15,9). | ||
link(6,15).link(15,6). | ||
link(18,19).link(19,18). | ||
link(15,16).link(16,15). | ||
link(0,10).link(10,0). | ||
link(15,18).link(18,15). | ||
link(10,14).link(14,10). | ||
link(7,11).link(11,7). | ||
link(10,13).link(13,10). | ||
link(0,15).link(15,0). | ||
link(11,19).link(19,11). | ||
link(7,8).link(8,7). | ||
link(5,15).link(15,5). | ||
link(3,17).link(17,3). | ||
link(1,18).link(18,1). | ||
link(0,18).link(18,0). | ||
link(3,16).link(16,3). | ||
link(3,9).link(9,3). | ||
link(12,13).link(13,12). | ||
link(1,6).link(6,1). | ||
link(8,18).link(18,8). | ||
link(6,8).link(8,6). | ||
link(0,8).link(8,0). | ||
link(3,15).link(15,3). | ||
link(0,3).link(3,0). | ||
link(17,19).link(19,17). | ||
link(2,11).link(11,2). | ||
link(7,9).link(9,7). | ||
link(13,15).link(15,13). | ||
link(6,10).link(10,6). |
86 changes: 86 additions & 0 deletions
86
src/test/resources/PreviouslyProblematic/vehicle_normal_small.asp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,86 @@ | ||
% A very simple example, how to encode object oriented models in ASP | ||
% we have n possible objects (which are of a specific class or not used at all) | ||
% an object is identified by an integer | ||
% in this example there a 3 classes(bicycle, tricycle and wheel), 1 association and 1 attribute | ||
% association vehicle(V,W) | ||
% a bicycle must have 2 wheels, a tricycle must have 3 wheels, | ||
% a wheel must have a vehicle (i.e. bicycle or tricycle) assigned | ||
% attribute: wheel_size wheels have sizes (small,medium,large) | ||
% 1 constraint: the wheels belonging to the same vehicle must have the same size | ||
|
||
%#const n = 5. | ||
%object(1..n). | ||
object(1). | ||
object(2). | ||
object(3). | ||
object(4). | ||
object(5). | ||
|
||
% restrict search space | ||
%object_type(1,unused). | ||
%object_type(2,unused). | ||
%object_type(3,unused). | ||
%object_type(4,unused). | ||
%object_type(5,unused). | ||
|
||
|
||
|
||
type(wheel). | ||
type(bicycle). | ||
type(tricycle). | ||
type(unused). | ||
size(small). | ||
size(medium). | ||
size(large). | ||
|
||
%%0 { object_type(O,T):type(T)} 1 :- object(O). | ||
%object_type(O,unused) :- object(O), not object_type(O,bicycle), not object_type(O,tricycle), not object_type(O,wheel). | ||
%object_type(O,wheel) :- object(O), not object_type(O,bicycle), not object_type(O,tricycle), not object_type(O,unused). | ||
%object_type(O,bicycle) :- object(O), not object_type(O,wheel), not object_type(O,tricycle), not object_type(O,unused). | ||
%object_type(O,tricycle) :- object(O), not object_type(O,bicycle), not object_type(O,wheel), not object_type(O,unused). | ||
|
||
% adoptions to use unique-rule head constraints | ||
% first, make each rule head unique | ||
object_type1(O,unused) :- object(O), not object_type3(O,bicycle), not object_type4(O,tricycle), not object_type2(O,wheel). | ||
object_type2(O,wheel) :- object(O), not object_type3(O,bicycle), not object_type4(O,tricycle), not object_type1(O,unused). | ||
object_type3(O,bicycle) :- object(O), not object_type2(O,wheel), not object_type4(O,tricycle), not object_type1(O,unused). | ||
object_type4(O,tricycle) :- object(O), not object_type3(O,bicycle), not object_type2(O,wheel), not object_type1(O,unused). | ||
:- object(X), not object_type1(X,unused), not object_type2(X,wheel), not object_type3(X,bicycle), not object_type4(X,tricycle). | ||
% redirect to object_type/2 | ||
object_type(X,T) :- object_type1(X,T). | ||
object_type(X,T) :- object_type2(X,T). | ||
object_type(X,T) :- object_type3(X,T). | ||
object_type(X,T) :- object_type4(X,T). | ||
:- vehicle(V), not object_type(V,bicycle), not object_type(V,tricycle). | ||
|
||
% assign wheels to vehicles | ||
%1 { vehicle_wheel(O,W):T!=wheel,object_type(O,T) } 1 :- object_type(W,wheel). | ||
vehicle(V) :- object_type(V,bicycle). | ||
vehicle(V) :- object_type(V,tricycle). | ||
|
||
|
||
vehicle_wheel(V,W) :- object_type(W,wheel), vehicle(V), not not_vehicle_wheel(V,W). | ||
not_vehicle_wheel(V,W) :- object_type(W,wheel), vehicle(V), not vehicle_wheel(V,W). | ||
:- object_type(W,wheel), vehicle_wheel(V1,W), vehicle_wheel(V2,W), V1 != V2. | ||
wheel_has_vehicle(W) :- vehicle_wheel(X_,W). | ||
:- object_type(W,wheel), not wheel_has_vehicle(W). | ||
|
||
% wheel size | ||
%1 { wheel_size(W,S):size(S) } 1 :- object_type(W,wheel). | ||
wheel_size(W,S) :- object_type(W,wheel), size(S), not not_wheel_size(W,S). | ||
not_wheel_size(W,S) :- object_type(W,wheel), size(S), not wheel_size(W,S). | ||
:- object_type(W,wheel), wheel_size(W,S1), wheel_size(W,S2), S1 != S2. | ||
wheel_has_size(W) :- wheel_size(W,X_). | ||
:- object_type(W,wheel), not wheel_has_size(W). | ||
|
||
% cardinality restrictions for vehicle_wheel | ||
%vehicle_has_wheel(V) :- vehicle(V), vehicle_wheel(V,_). | ||
vehicle_has_2_wheels(V) :- vehicle(V), vehicle_wheel(V,W1), vehicle_wheel(V,W2), W1 != W2. | ||
vehicle_has_3_wheels(V) :- vehicle(V), vehicle_wheel(V,W1), vehicle_wheel(V,W2), vehicle_wheel(V,W3), W1 != W2, W1 != W3, W2 != W3. | ||
:- object_type(B,bicycle), not vehicle_has_2_wheels(B). | ||
:- object_type(B,bicycle), vehicle_wheel(B,W1), vehicle_wheel(B,W2), vehicle_wheel(B,W3), W1 != W2, W1 != W3, W2 != W3. | ||
:- object_type(T,tricycle), not vehicle_has_3_wheels(T). | ||
:- object_type(T,tricycle), vehicle_wheel(B,W1), vehicle_wheel(B,W2), vehicle_wheel(B,W3), vehicle_wheel(B,W4), W1 != W2, W1 != W3, W1 != W4, W2 != W3, W2 != W4, W3 != W4. | ||
|
||
% constraint wheel size | ||
:-wheel_size(W1,S1),wheel_size(W2,S2),vehicle_wheel(V,W1),vehicle_wheel(V,W2),S1!=S2. |