From 326bf4b93fa6e75b88b14647a9a9e7d4956f602c Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Sun, 30 Jul 2023 17:40:17 +0200 Subject: [PATCH] Deleted java files from doc --- .../sts/sts/aiger/AigerCoiTest.java | 69 ---------------- .../sts/sts/aiger/AigerConstPropTest.java | 75 ------------------ .../Formalisms/sts/sts/dsl/StsDslTest.java | 64 --------------- .../sts/sts/parser/StsParserTest.java | 78 ------------------- 4 files changed, 286 deletions(-) delete mode 100644 doc/wiki/docs/Formalisms/sts/sts/aiger/AigerCoiTest.java delete mode 100644 doc/wiki/docs/Formalisms/sts/sts/aiger/AigerConstPropTest.java delete mode 100644 doc/wiki/docs/Formalisms/sts/sts/dsl/StsDslTest.java delete mode 100644 doc/wiki/docs/Formalisms/sts/sts/parser/StsParserTest.java diff --git a/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerCoiTest.java b/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerCoiTest.java deleted file mode 100644 index 6a0f80161d..0000000000 --- a/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerCoiTest.java +++ /dev/null @@ -1,69 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.sts.aiger; - -import java.io.IOException; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.Assert; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import hu.bme.mit.theta.sts.aiger.elements.AigerSystem; -import hu.bme.mit.theta.sts.aiger.utils.AigerCoi; - -@RunWith(Parameterized.class) -public class AigerCoiTest { - - @Parameter(value = 0) - public String path; - - @Parameter(value = 1) - public int sizeOld; - - @Parameter(value = 2) - public int sizeNew; - - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"coi1.aag", 8, 3}, - - {"coi2.aag", 5, 3}, - - {"simple.aag", 6, 5}, - - {"simple2.aag", 6, 5}, - - {"simple3.aag", 7, 6}, - - }); - } - - @Test - public void test() throws IOException { - final AigerSystem system = AigerParser.parse("src/test/resources/" + path); - Assert.assertEquals(sizeOld, system.getNodes().size()); - AigerCoi.apply(system); - Assert.assertEquals(sizeNew, system.getNodes().size()); - } - -} diff --git a/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerConstPropTest.java b/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerConstPropTest.java deleted file mode 100644 index c5108d4607..0000000000 --- a/doc/wiki/docs/Formalisms/sts/sts/aiger/AigerConstPropTest.java +++ /dev/null @@ -1,75 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.sts.aiger; - -import java.io.IOException; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.Assert; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import hu.bme.mit.theta.sts.aiger.elements.AigerSystem; -import hu.bme.mit.theta.sts.aiger.utils.AigerCoi; -import hu.bme.mit.theta.sts.aiger.utils.AigerConstProp; - -@RunWith(Parameterized.class) -public class AigerConstPropTest { - - @Parameter(value = 0) - public String path; - - @Parameter(value = 1) - public int sizeOld; - - @Parameter(value = 2) - public int sizeNew; - - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"coi1.aag", 8, 3}, - - {"coi2.aag", 5, 1}, - - {"simple.aag", 6, 5}, - - {"simple2.aag", 6, 5}, - - {"simple3.aag", 7, 6}, - - {"constprop1.aag", 6, 1}, - - {"constprop2.aag", 6, 4}, - - }); - } - - @Test - public void test() throws IOException { - final AigerSystem system = AigerParser.parse("src/test/resources/" + path); - Assert.assertEquals(sizeOld, system.getNodes().size()); - AigerConstProp.apply(system); - AigerCoi.apply(system); - Assert.assertEquals(sizeNew, system.getNodes().size()); - } - -} diff --git a/doc/wiki/docs/Formalisms/sts/sts/dsl/StsDslTest.java b/doc/wiki/docs/Formalisms/sts/sts/dsl/StsDslTest.java deleted file mode 100644 index 3e60207e28..0000000000 --- a/doc/wiki/docs/Formalisms/sts/sts/dsl/StsDslTest.java +++ /dev/null @@ -1,64 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.sts.dsl; - -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.Assert; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import hu.bme.mit.theta.sts.STS; - -@RunWith(Parameterized.class) -public class StsDslTest { - - @Parameter(0) - public String filepath; - - @Parameter(1) - public String propertyName; - - @Parameter(2) - public int varCount; - - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"/readerswriters.system", "safe", 3}, - - {"/simple1.system", "safe", 2} - - }); - } - - @Test - public void test() throws FileNotFoundException, IOException { - final InputStream inputStream = StsDslTest.class.getResourceAsStream(filepath); - final StsSpec spec = StsDslManager.createStsSpec(inputStream); - final STS sts = spec.createProp(propertyName); - Assert.assertEquals(varCount, sts.getVars().size()); - } - -} diff --git a/doc/wiki/docs/Formalisms/sts/sts/parser/StsParserTest.java b/doc/wiki/docs/Formalisms/sts/sts/parser/StsParserTest.java deleted file mode 100644 index 9c2c83a039..0000000000 --- a/doc/wiki/docs/Formalisms/sts/sts/parser/StsParserTest.java +++ /dev/null @@ -1,78 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.sts.parser; - -import java.io.FileNotFoundException; -import java.io.FileReader; -import java.io.IOException; -import java.io.Reader; -import java.util.Arrays; -import java.util.Collection; - -import org.junit.After; -import org.junit.Assert; -import org.junit.Before; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import hu.bme.mit.theta.sts.STS; - -@RunWith(Parameterized.class) -public final class StsParserTest { - - @Parameter(0) - public String filepath; - - @Parameter(1) - public int vars; - - private Reader reader; - private StsParser parser; - - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - - {"src/test/resources/simple1.lisp.sts", 2}, - - {"src/test/resources/readerswriters.lisp.sts", 3}, - - }); - } - - @Before - public void before() throws FileNotFoundException { - reader = new FileReader(filepath); - parser = new StsParser(reader); - } - - @After - public void after() throws IOException { - reader.close(); - } - - @Test - public void test() { - // Act - final STS sts = parser.sts(); - System.out.println(sts); - Assert.assertEquals(vars, sts.getVars().size()); - } - -}