Merge branch 'misc/loose-ends'

.github/workflows/main.yml

@@ -129,13 +129,13 @@ jobs:
           echo 'config solver="sat4j"' >> $line
         done
     - name: SAT4j part 1
-      run: java -jar logic-compiler.jar sat/problem_sat.logic
+      run: java -jar logic-compiler.jar sat/problem_sat.logic result.txt
     - name: Check for correct output 1
       run: diff result.txt sat/solution_sat.txt  # will fail if diffs
     - name: Quick cleanup
       run: rm result.txt
     - name: SAT4j part 2
-      run: java -jar logic-compiler.jar sat/problem_unsat.logic
+      run: java -jar logic-compiler.jar sat/problem_unsat.logic result.txt
     - name: Check for correct output 2
       run: diff result.txt sat/solution_unsat.txt
 

README.md

@@ -1,32 +1,18 @@
-# Logic app
-(better name needed)
+# CAIR Logic Platform
 
 ## Purpose
 The goal of this repo is to provide a platform for generic logic operations (checking for consistency, validity, explanations, etc.) by way of an easy-to-use DSL. 
 
 ## Mission
 The purpose is achieved by way of three parts:
 - The DSL specification and generator (`za.org.cair.logic_app`)
-- An IDE plugin (`za.org.cair.logic_app.ide`)
+- An IDE plugin (`za.org.cair.logic_app.ide`) (Not implemented)
 - A webapp editor (`za.org.cair.logic_app.web`)
 
 ## Usage
 
-### On the CLI
-
-Xtext compilers are not typically used on the command like (like e.g. `gcc` and `javac`) so support (especially in CI contexts) is very limited. Through some shady hacks I got it working (for now). 
-
-Download the compiler jar from the [CLI logic lang compiler workflow](https://github.com/Koellewe/logic-app/actions?query=workflow%3A%22Build+CLI+logic+lang+compiler%22) build artifacts. Create a file written in the specified logic language (with `.logic` as file extension). Compile as follows:
-
-```sh
-java -jar logic-compiler.jar example.logic
-```
-
-Ignore the reflection warnings. They are caused in Java 11 onwards by a lib xtext depends on and will be updated once the developers there get their act together. [More info](https://github.com/eclipse/xtext-core/issues/506).
-
-
-### As library / on Web / in IDE
-
-TODO
+See the [wiki entry](https://github.com/Koellewe/logic-app/wiki/Running-and-Deployment).
 
+## More info
 
+See the [wiki](https://github.com/Koellewe/logic-app/wiki).

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/LogicLangHelper.java

@@ -1,5 +1,7 @@
 package za.org.cair.logic_app;
 
+import java.util.Random;
+
 import org.eclipse.emf.mwe2.language.mwe2.impl.BooleanLiteralImplCustom;
 
 import za.org.cair.logic_app.logicLang.BooleanLiteral;
@@ -19,6 +21,9 @@
 import za.org.cair.logic_app.logicLang.impl.NegationImpl;
 
 public class LogicLangHelper {
+
+	// used for #randomHash()
+	private static Random rand = new Random();
 
 	/**
 	 * Checks if the sentence is complex (i.e. has a left and right side)
@@ -165,4 +170,11 @@ public static Sentence copyOf(Sentence sent) {
 		}
 	}
 
+	/**
+	 * Create a random hash. Useful for e.g. concurrent filesystem access
+	 */
+	public static String randomHash(int basis) {
+		return Integer.toHexString(basis * (rand.nextInt()+1));
+	}
+
 }

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/external/Sat4j.xtend

@@ -10,11 +10,11 @@ import java.io.BufferedWriter
 import java.util.HashMap
 import java.io.BufferedReader
 import java.io.InputStreamReader
+import za.org.cair.logic_app.LogicLangHelper
 
 class Sat4j {
 
 	val SAT4J_JAR = "sat4j.jar"
-	val DIMACS_FILE = "dimacs.cnf"
 
 	List<Proposition> inputProps
 
@@ -35,9 +35,11 @@ class Sat4j {
 	 */
 	def Pair<Boolean, Map<String, Boolean>> solve(){
 
+		val dimacsFile = LogicLangHelper.randomHash(inputProps.hashCode())+".cnf";
+
 		// create dimacs file
 		val dimacsContent = new CNFConverter().convertToDIMACS(inputProps)
-		val writer = new BufferedWriter(new FileWriter("dimacs.cnf"))
+		val writer = new BufferedWriter(new FileWriter(dimacsFile))
 		writer.write(dimacsContent)
 		writer.close()
 
@@ -53,7 +55,7 @@ class Sat4j {
 		}
 
 		// run sat4j
-		val proc = Runtime.runtime.exec("java -jar "+SAT4J_JAR+" "+DIMACS_FILE)
+		val proc = Runtime.runtime.exec("java -jar "+SAT4J_JAR+" "+dimacsFile)
 		if (proc.errorStream.read != -1){
 			throw new RuntimeException("Sat4j failed to solve.")
 		}
@@ -86,7 +88,7 @@ class Sat4j {
 		}
 
 		// clean up
-		new File(DIMACS_FILE).delete()
+		new File(dimacsFile).delete()
 
 		// finish
 		return Pair.of(satis, solution)

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/generator/Main.java

@@ -1,5 +1,9 @@
 package za.org.cair.logic_app.generator;
 
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map.Entry;
@@ -20,6 +24,7 @@
 import com.google.inject.Injector;
 import com.google.inject.Provider;
 
+import za.org.cair.logic_app.LogicLangHelper;
 import za.org.cair.logic_app.LogicLangStandaloneSetup;
 
 public class Main {
@@ -96,4 +101,30 @@ protected void runGenerator(String[] args) {
 
 		}
 	}
+
+	/**
+	 * These methods are used to run validation on some source code.
+	 * They are needed, because for some bizarre reason validation doesn't
+	 * work in JUnit 5 test context. 
+	 * @param src source code
+	 * @return A set of warnings and errors produced by the validator. 
+	 * @throws IOException If there was an error creating or deleting temporary files.
+	 */
+	public static List<Issue> justValidate(String src) throws IOException{
+		Injector injector = new LogicLangStandaloneSetup().createInjectorAndDoEMFRegistration();
+		Main main = injector.getInstance(Main.class);
+		return main.internalJustValidate(src);
+	}
+
+	private List<Issue> internalJustValidate(String src) throws IOException{
+		String tmpFile = LogicLangHelper.randomHash(src.hashCode())+".logic";
+		BufferedWriter writer = new BufferedWriter(new FileWriter(tmpFile));
+		writer.write(src);
+		writer.close();
+
+		Resource resource = resourceSetProvider.get().getResource(URI.createFileURI(tmpFile), true);
+		List<Issue> issues = validator.validate(resource, CheckMode.ALL, CancelIndicator.NullImpl);
+		new File(tmpFile).delete();
+		return issues;
+	}
 }

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/validation/CommandValidator.java

@@ -20,7 +20,7 @@ public void checkForCommands(Model model) {
 		if(model.getCommands().size() == 0) {
 			warning("No commands specified. Nothing to do.", 
 					LogicLangPackage.Literals.MODEL__COMMANDS, 
-					LogicLangValidator.NO_COMMANDS);
+					LogicLangValidator.ISSUE_NO_COMMANDS);
 		}
 	}
 

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/validation/ConfigValidator.java

@@ -1,21 +1,29 @@
 package za.org.cair.logic_app.validation;
 
+import java.util.HashSet;
+
 import org.eclipse.xtext.util.Arrays;
 import org.eclipse.xtext.validation.AbstractDeclarativeValidator;
 import org.eclipse.xtext.validation.Check;
 import org.eclipse.xtext.validation.CheckType;
 import org.eclipse.xtext.validation.EValidatorRegistrar;
 
+import za.org.cair.logic_app.LogicLangHelper;
+import za.org.cair.logic_app.logicLang.BooleanLiteral;
 import za.org.cair.logic_app.logicLang.Command;
 import za.org.cair.logic_app.logicLang.Config;
 import za.org.cair.logic_app.logicLang.ConfigKey;
 import za.org.cair.logic_app.logicLang.LogicLangPackage;
 import za.org.cair.logic_app.logicLang.Model;
+import za.org.cair.logic_app.logicLang.Negation;
+import za.org.cair.logic_app.logicLang.Proposition;
+import za.org.cair.logic_app.logicLang.Sentence;
 import za.org.cair.logic_app.logicLang.SolutionRequest;
 import za.org.cair.logic_app.logicLang.SolveCommand;
 
 public class ConfigValidator extends AbstractDeclarativeValidator {
 
+	// supported SAT solvers to be listed here
 	private static String[] SOLVERS = new String[] {"sat4j"};
 
 	@Override
@@ -25,16 +33,26 @@ public void register(EValidatorRegistrar registrar) {
 
 	@Check(CheckType.NORMAL)
 	public void checkConfigUnique(Model model) {
-		// TODO
+		HashSet<ConfigKey> configs = new HashSet<>();
+		for (Config cfg : model.getConfig()) {
+			if (configs.contains(cfg.getKey())) { // duplicate key
+				error("Duplicate config item for key: "+cfg.getKey().getName(),
+						cfg, LogicLangPackage.Literals.CONFIG__KEY,
+						LogicLangValidator.ISSUE_CONFIG_DUPE);
+			} else {
+				configs.add(cfg.getKey());
+			}
+		}
 	}
 
 	@Check(CheckType.NORMAL) 
 	public void checkConfig(Config cfg) {
 		if (cfg.getKey() == ConfigKey.SOLVER) {
+			// check that solver is valid
 			if (!Arrays.contains(SOLVERS, cfg.getValue())) {
 				error("Solver '"+cfg.getValue()+"' not supported.",
 						cfg, LogicLangPackage.Literals.CONFIG__VALUE,
-						LogicLangValidator.CONFIG_ISSUE);
+						LogicLangValidator.ISSUE_UNSUPPORTED_SOLVER);
 			}
 		}// more cfg checks here
 	}
@@ -62,9 +80,34 @@ public void checkSolverSpecified(Model model) {
 			if (!aptConfig) {
 				error("No solver specified in config.",
 						commandInQuestion, LogicLangPackage.Literals.SOLVE_COMMAND__WHAT,
-						LogicLangValidator.SOLVER_ISSUE);
+						LogicLangValidator.ISSUE_NO_SOLVER);
 			}
+
+			// check for boolean literals
+			for (Proposition prop : model.getPropositions()) {
+				warnBooleanLiteral(prop.getSentence());
+			}
+
 		}
 	}
 
+	/**
+	 * Recursively find boolean literals and throw a warning for each.
+	 * Rationale: SAT solvers interpret "True" and "False" as variables and
+	 * so may end up assigning True=False to find satisfiability. Best to do
+	 * some math and drop the literals.  
+	 */
+	private void warnBooleanLiteral(Sentence sent) {
+		if (sent instanceof BooleanLiteral) {
+			warning("Do not use boolean literals with SAT solving", sent,
+					LogicLangPackage.Literals.BOOLEAN_LITERAL__TRUTH,
+					LogicLangValidator.ISSUE_SAT_BOOL);
+		}else if (LogicLangHelper.isComplexSentence(sent)) {
+			warnBooleanLiteral(LogicLangHelper.getLeftSide(sent));
+			warnBooleanLiteral(LogicLangHelper.getRightSide(sent));
+		}else if (sent instanceof Negation) {
+			warnBooleanLiteral(((Negation) sent).getExpression());
+		} // else BooleanVariable
+	}
+
 }

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/validation/LogicLangValidator.java

@@ -23,19 +23,21 @@
 public class LogicLangValidator extends AbstractLogicLangValidator {
 
 	// List all validation issue codes here:
-	public static final String NO_PROPOSITIONS = "noPropositions";
-	public static final String NO_COMMANDS = "noCommands";
-	public static final String INCONSISTENT_SYMBOLOGY = "inconsistentSymbology";
-	public static final String CONFIG_ISSUE = "configIssue";
-	public static final String SOLVER_ISSUE = "solverIssue";
+	public static final String ISSUE_NO_PROPOSITIONS = "noPropositions";
+	public static final String ISSUE_NO_COMMANDS = "noCommands";
+	public static final String ISSUE_INCONSISTENT_SYMBOLOGY = "inconsistentSymbology";
+	public static final String ISSUE_CONFIG_DUPE = "configDuplicate";
+	public static final String ISSUE_UNSUPPORTED_SOLVER = "unsupportedSolver";
+	public static final String ISSUE_NO_SOLVER = "noSolver";
+	public static final String ISSUE_SAT_BOOL = "satBool";
 
 	@Check(CheckType.NORMAL) // only check at build-time
 	public void checkForPropositions(Model model) {
 		if (model.getPropositions().size() == 0) {
 			warning("No propositions specified. No input to work on.",
 					// Note: LogicLangPackage stuff is auto-generated from the grammar
 					LogicLangPackage.Literals.MODEL__PROPOSITIONS,
-					LogicLangValidator.NO_PROPOSITIONS);
+					LogicLangValidator.ISSUE_NO_PROPOSITIONS);
 		}
 	}
 

za.org.cair.logic_app/src/main/java/za/org/cair/logic_app/validation/VariantValidator.java

@@ -92,7 +92,7 @@ private void checkSymbolInconsistency(AtomicBoolean checkingStarted, AtomicBoole
 			if (thisVariant != runningVariant.get())
 				warning("Inconsistent logic symbology", where, 
 						appropriateRef(where), 
-						LogicLangValidator.INCONSISTENT_SYMBOLOGY);
+						LogicLangValidator.ISSUE_INCONSISTENT_SYMBOLOGY);
 			// either case do nothing (continue checking)
 
 		}else { // this is the first ever check: set this variant to the running variant

za.org.cair.logic_app/src/test/java/za/org/cair/logic_app/tests/CommandsTest.xtend

@@ -1,40 +1,46 @@
 package za.org.cair.logic_app.tests
 
-import org.junit.jupiter.api.^extension.ExtendWith
-import org.eclipse.xtext.testing.extensions.InjectionExtension
 import org.eclipse.xtext.testing.InjectWith
-import javax.inject.Inject
-import org.eclipse.xtext.testing.util.ParseHelper
-import za.org.cair.logic_app.logicLang.Model
-import static org.junit.Assert.assertNotNull
+import org.eclipse.xtext.testing.extensions.InjectionExtension
 import org.junit.jupiter.api.Test
-//import org.eclipse.xtext.testing.validation.ValidationTestHelper
-//import za.org.cair.logic_app.logicLang.LogicLangPackage
-//import za.org.cair.logic_app.validation.LogicLangValidator
+import org.junit.jupiter.api.^extension.ExtendWith
+import za.org.cair.logic_app.validation.LogicLangValidator
 
 @ExtendWith(InjectionExtension)
 @InjectWith(LogicLangInjectorProvider)
 class CommandsTest {
-
-	@Inject
-	ParseHelper<Model> parseHelper
-
-//	@Inject
-//	ValidationTestHelper validationHelper
 
 	@Test
 	def void testNoCommands() {
-		val result = parseHelper.parse('''
+
+		val src = '''
 			prop A | B
 			prop C -> D
-		''')
-		assertNotNull(result)
-//		val valres = validationHelper.validate(result)
-//		println('valresses: ' + valres.size)
-//		
-//		TestingHelper.assertWarning(result, LogicLangValidator.NO_COMMANDS)
-
-		// TODO: validation not working yet. Removing this test for now.
+		'''
+
+		TestingHelper.assertIssue(src, LogicLangValidator.ISSUE_NO_COMMANDS);
 
 	}
+
+	@Test
+	def void satNoSolver(){
+		TestingHelper.assertIssue('''
+			prop Ayy | Bee
+			cmd solve satisfiability
+		''',
+			LogicLangValidator.ISSUE_NO_SOLVER
+		)
+	}
+
+	@Test
+	def void satBool(){
+		TestingHelper.assertIssue('''
+			prop var1 & True
+			cmd solve satisfiability
+			config solver='sat4j'
+		''',
+			LogicLangValidator.ISSUE_SAT_BOOL
+		)
+	}
+
 }