minor bug fixes for headless agree

com.rockwellcollins.atc.agree.analysis/META-INF/MANIFEST.MF

@@ -5,19 +5,13 @@ Bundle-SymbolicName: com.rockwellcollins.atc.agree.analysis; singleton:=true
 Bundle-Version: 2.10.1.qualifier
 Bundle-Activator: com.rockwellcollins.atc.agree.analysis.Activator
 Bundle-Vendor: Rockwell Collins, Inc.
-Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,4.0.0)",
- org.eclipse.emf.transaction;bundle-version="[1.9.0,2.0.0)",
- org.eclipse.core.runtime;bundle-version="[3.20.0,4.0.0)",
- org.osate.aadl2.modelsupport;bundle-version="[7.0.0,8.0.0)",
+Require-Bundle: org.osate.aadl2.modelsupport;bundle-version="[7.0.0,8.0.0)",
  org.eclipse.ui.console;bundle-version="[3.5.100,4.0.0)",
- org.eclipse.core.expressions;bundle-version="[3.4.401,4.0.0)",
  org.osate.aadl2;bundle-version="[5.0.0,6.0.0)",
  org.osate.ui;bundle-version="[6.0.0,7.0.0)",
  org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)",
- com.rockwellcollins.atc.agree;bundle-version="[3.1.0,4.0.0)",
  com.rockwellcollins.atc.agree.ui;bundle-version="[3.2.0,4.0.0)",
  org.osate.ge;bundle-version="[3.0.0,4.0.0)",
- org.eclipse.emf.ecore;bundle-version="[2.23.0,3.0.0)",
  com.collins.trustedsystems.z3;bundle-version="[4.0.0,5.0.0)",
  org.osate.aadl2.instantiation;bundle-version="[3.0.0,4.0.0)",
  org.osate.annexsupport;bundle-version="[4.0.1,5.0.0)",
@@ -27,7 +21,6 @@ Bundle-RequiredExecutionEnvironment: JavaSE-17
 Bundle-ActivationPolicy: lazy
 Bundle-ClassPath: .,
  lib/gson.jar
-Import-Package: org.apache.commons.lang;version="[2.6.0,3.0.0)"
 Export-Package: com.rockwellcollins.atc.agree.analysis;version="2.10.1",
  com.rockwellcollins.atc.agree.analysis.ast;version="2.10.1",
  com.rockwellcollins.atc.agree.analysis.ast.visitors;version="2.10.1",

com.rockwellcollins.atc.agree.cli/META-INF/MANIFEST.MF

@@ -5,11 +5,7 @@ Bundle-SymbolicName: com.rockwellcollins.atc.agree.cli;singleton:=true
 Bundle-Version: 1.0.1.qualifier
 Bundle-Activator: com.rockwellcollins.atc.agree.cli.Activator
 Bundle-Vendor: ROCKWELLCOLLINS
-Require-Bundle: org.eclipse.ui,
- org.eclipse.core.runtime,
- org.eclipse.emf.ecore;bundle-version="2.27.0",
- org.eclipse.xtext,
- org.osate.xtext.aadl2,
+Require-Bundle: org.osate.xtext.aadl2,
  com.rockwellcollins.atc.agree,
  org.osate.aadl2,
  org.osate.pluginsupport,

com.rockwellcollins.atc.agree.cli/README.md

@@ -22,7 +22,7 @@ AGREE can be run from the command line.  All AGREE tool preferences, along with
 | -noInductiveCounterexamples        | optional, do not generate inductive counterexamples | 
 | -noSplash                          | optional, hide the splash screen | 
 | -o,--output <arg>                  | required, output JSON file absolute path | 
-| -p,--project <arg>                 | required, project path (relative to workspace) | 
+| -p,--projectPath <arg>             | required, project path (relative to workspace) | 
 | -s,--solver <arg>                  | optional, SMT solver, default SMTInterpol | 
 | -strategy <arg>                    | required, verification strategy (single, all, monolithic, realizability) | 
 | -t,--timeout <arg>                 | optional, timeout (ms), default 100 | 
@@ -31,10 +31,10 @@ AGREE can be run from the command line.  All AGREE tool preferences, along with
 
 # Example
 
-Using the AGREE toy_example to demonstrate usage, assume the project folder is located at C:\models\toy_example.  To perform a single layer analysis on the top_level.impl component in the Integer package, run the following command:
+Using the AGREE toy_example to demonstrate usage, assume the project folder is located at C:\models\toy_example.  To perform a single layer analysis on the top_level.impl component in the Integer_Toy package, run the following command:
 
-`osate.exe -application com.rockwellcollins.atc.agree.cli.Agree -noSplash -data C:/models -p Toy_Example -c Integer_Toy::top_level.Impl -strategy single -o C:/models/toy_example/output/AgreeResults.json`
+`osate.exe -application com.rockwellcollins.atc.agree.cli.Agree -noSplash -data C:/models -p toy_example -c Integer_Toy::top_level.Impl -strategy single -o C:/models/toy_example/output/AgreeResults.json`
 
 Executing `osatec.exe` with the same arguments will capture debug output in the terminal.
 
-The AGREE output will be written to a file in json format if the `-o` argument is provided.
+The AGREE output will be written to a file in json format if the `-o` argument is provided.  If the output directory does not exist, it will be created.

com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Agree.java

@@ -1,6 +1,9 @@
 package com.rockwellcollins.atc.agree.cli;
 
 import java.io.File;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -98,7 +101,7 @@ public class Agree implements IApplication {
 	private final static String DATA = "data";
 	private final static String APPLICATION = "application";
 	private final static String NO_SPLASH = "noSplash";
-	private final static String PROJECT = "p";
+	private final static String PROJECT_PATH = "p";
 	private final static String COMP_IMPL = "c";
 	private final static String OUTPUT = "o";
 	private final static String FILES = "f";
@@ -149,7 +152,7 @@ public Object start(IApplicationContext context) throws Exception {
 		output.setDate((new Date()).toString());
 
 		// Process command line options
-		String workspace = ResourcesPlugin.getWorkspace().getRoot().getLocation().toString();
+		final String workspace = ResourcesPlugin.getWorkspace().getRoot().getLocation().toString();
 		String projPath = null;
 		String component = null;
 		String outputPath = null;
@@ -185,7 +188,7 @@ public Object start(IApplicationContext context) throws Exception {
 		options.addOption(DATA, true, "required, path of workspace");
 		options.addOption(APPLICATION, true,
 				"required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree)");
-		options.addOption(PROJECT, "project", true, "required, project path (relative to workspace)");
+		options.addOption(PROJECT_PATH, "projectPath", true, "required, project path (relative to workspace)");
 		options.addOption(COMP_IMPL, "compImpl", true, "required, qualified component implementation name");
 		options.addOption(OUTPUT, "output", true, "required, output JSON file absolute path");
 		Option option = new Option(FILES, "files", true, "optional, supplementary AADL files (absolute paths)");
@@ -216,33 +219,37 @@ public Object start(IApplicationContext context) throws Exception {
 
 			if (commandLine.hasOption(HELP)) {
 				exit = true;
-				output.setStatus(AgreeOutput.INTERRUPTED);
 			}
 			if (workspace == null || workspace.isBlank()) {
 				exit = true;
-				output.setStatus(AgreeOutput.INTERRUPTED);
 				output.addStatusMessage("A workspace must be specified.");
 			}
 			if (commandLine.hasOption(COMP_IMPL)) {
 				component = commandLine.getOptionValue(COMP_IMPL);
 				output.setComponent(component);
 				// expects qualified name
 				if (!component.contains("::")) {
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Component implementation qualified name must be specified.");
 					exit = true;
 				}
 			}
-			if (commandLine.hasOption(PROJECT)) {
-				projPath = workspace + File.separator + commandLine.getOptionValue(PROJECT);
-				output.setProject(projPath);
+			if (commandLine.hasOption(PROJECT_PATH)) {
+				projPath = commandLine.getOptionValue(PROJECT_PATH);
+				final Path projectPath = Paths.get(workspace, projPath);
+				if (!Files.isDirectory(projectPath)) {
+					exit = true;
+					output.addStatusMessage("Specified project directory doesn't exist: " + projectPath.toString());
+				} else {
+					output.setProject(projPath);
+				}
 			} else {
-				output.setStatus(AgreeOutput.INTERRUPTED);
 				output.addStatusMessage("Project path must be specified.");
 				exit = true;
 			}
 			if (commandLine.hasOption(OUTPUT)) {
 				outputPath = commandLine.getOptionValue(OUTPUT);
+				// Make sure output directory exists
+				new File(outputPath).mkdirs();
 			}
 			if (commandLine.hasOption(FILES)) {
 				fileArray = commandLine.getOptionValues(FILES);
@@ -263,12 +270,10 @@ public Object start(IApplicationContext context) throws Exception {
 					break;
 				default:
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid verification strategy.  " + commandLine.getOptionValue(STRATEGY) + " is not supported.");
 				}
 			} else {
 				exit = true;
-				output.setStatus(AgreeOutput.INTERRUPTED);
 				output.addStatusMessage("A verification type must be specified (single, all, monolithic, realizability).");
 			}
 			if (commandLine.hasOption(MODEL_CHECKER)) {
@@ -287,7 +292,6 @@ public Object start(IApplicationContext context) throws Exception {
 					break;
 				default:
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid model checker.  " + commandLine.getOptionValue(MODEL_CHECKER) + " is not supported. Valid options are: JKind, Kind2, Kind2Remote, Sally.");
 				}
 			}
@@ -316,7 +320,6 @@ public Object start(IApplicationContext context) throws Exception {
 					break;
 				default:
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid solver.  " + commandLine.getOptionValue(SOLVER) + " is not supported.  Valid options are: SMTInterpol, Yices, Yices2, Z3, CVC4, CVC5, dReal.");
 				}
 			}
@@ -350,7 +353,6 @@ public Object start(IApplicationContext context) throws Exception {
 					store.setValue(PreferenceConstants.PREF_DEPTH, i);
 				} catch (NumberFormatException e) {
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid maximum induction depth specified.  " + e.getMessage());
 				}
 			}
@@ -363,7 +365,6 @@ public Object start(IApplicationContext context) throws Exception {
 					store.setValue(PreferenceConstants.PREF_PDR_MAX, i);
 				} catch (NumberFormatException e) {
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid maximum PDR instances specified.  " + e.getMessage());
 				}
 			}
@@ -376,7 +377,6 @@ public Object start(IApplicationContext context) throws Exception {
 					store.setValue(PreferenceConstants.PREF_TIMEOUT, i);
 				} catch (NumberFormatException e) {
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid timeout specified.  " + e.getMessage());
 				}
 			}
@@ -389,7 +389,6 @@ public Object start(IApplicationContext context) throws Exception {
 					store.setValue(PreferenceConstants.PREF_CONSIST_DEPTH, i);
 				} catch (NumberFormatException e) {
 					exit = true;
-					output.setStatus(AgreeOutput.INTERRUPTED);
 					output.addStatusMessage("Invalid consistency depth specified.  " + e.getMessage());
 				}
 			}
@@ -417,6 +416,7 @@ public Object start(IApplicationContext context) throws Exception {
 		if (exit) {
 			final HelpFormatter formatter = new HelpFormatter();
 			formatter.printHelp("osate", options);
+			output.setStatus(AgreeOutput.INTERRUPTED);
 			Util.writeOutput(output, outputPath);
 			return IApplication.EXIT_OK;
 		}

com.rockwellcollins.atc.agree.cli/src/com/rockwellcollins/atc/agree/cli/Util.java

@@ -53,25 +53,33 @@ public class Util {
 	public static void loadProjectAadlFiles(String projPath, String[] libArray, XtextResourceSet resourceSet)
 			throws Exception {
 
-		final List<String> projectFiles = findFiles(Paths.get(projPath), "aadl");
-		final File projectRootDirectory = new File(projPath);
-		final File projectFile = new File(projectRootDirectory, ".project");
+		final String workspace = ResourcesPlugin.getWorkspace().getRoot().getLocation().toString();
+		final Path absProjPath = Paths.get(workspace, projPath);
+		final List<String> projectFiles = findFiles(absProjPath, "aadl");
+		final File projectFile = new File(absProjPath.toFile(), ".project");
 		final String projName = getProjectName(projectFile);
 
 		// Add project to workspace
 		addProjectToWorkspace(projPath, projName);
 
 		// Map project folder to project name (they could be different)
 		final Map<String, String> projMap = new HashMap<>();
-		final List<String> dotProjFiles = findFiles(projectRootDirectory.getParentFile().toPath(), "project");
+		Path topLevelDir = absProjPath;
+		for (int i = 0; i < URI.createURI(projPath).segmentCount() - 1; ++i) {
+			if (topLevelDir.getParent() != null) {
+				topLevelDir = topLevelDir.getParent();
+			}
+		}
+
+		final List<String> dotProjFiles = findFiles(topLevelDir, "project");
 		for (String dotProjFile : dotProjFiles) {
 			final File projFile = new File(dotProjFile);
 			projMap.put(getProjectName(projFile), projFile.getParentFile().getAbsolutePath());
 		}
 
 		for (String pFile : projectFiles) {
 			final File projFile = new File(pFile);
-			loadFile(projectRootDirectory, projName, projFile, resourceSet);
+			loadFile(absProjPath.toFile(), projName, projFile, resourceSet);
 		}
 
 		// load user specified AADL libs
@@ -130,10 +138,6 @@ public static SyntaxValidationResults validateResourceSet(XtextResourceSet resou
 
 	private static List<String> findFiles(Path path, String fileExtension) throws Exception {
 
-		if (!Files.isDirectory(path)) {
-			throw new IllegalArgumentException("Path must be a directory!");
-		}
-
 		final List<String> result;
 
 		try (Stream<Path> walk = Files.walk(path)) {

com.rockwellcollins.atc.agree.examples/examples/bscu/.project

@@ -3,7 +3,6 @@
 	<name>BSCU</name>
 	<comment></comment>
 	<projects>
-		<project>Plugin_Resources</project>
 	</projects>
 	<buildSpec>
 		<buildCommand>

com.rockwellcollins.atc.agree.examples/examples/car/.project

@@ -3,7 +3,6 @@
 	<name>Car</name>
 	<comment></comment>
 	<projects>
-		<project>Plugin_Resources</project>
 	</projects>
 	<buildSpec>
 		<buildCommand>

com.rockwellcollins.atc.agree.examples/examples/codependence/.project

@@ -3,7 +3,6 @@
 	<name>Codependence</name>
 	<comment></comment>
 	<projects>
-		<project>Plugin_Resources</project>
 	</projects>
 	<buildSpec>
 		<buildCommand>

com.rockwellcollins.atc.agree.examples/examples/microwave/.project

@@ -3,7 +3,6 @@
 	<name>Microwave</name>
 	<comment></comment>
 	<projects>
-		<project>Plugin_Resources</project>
 	</projects>
 	<buildSpec>
 		<buildCommand>

com.rockwellcollins.atc.agree.examples/examples/toy_example/.project

@@ -3,7 +3,6 @@
 	<name>Toy_Example</name>
 	<comment></comment>
 	<projects>
-		<project>Plugin_Resources</project>
 	</projects>
 	<buildSpec>
 		<buildCommand>

com.rockwellcollins.atc.agree.ui/META-INF/MANIFEST.MF

@@ -6,27 +6,14 @@ Bundle-Version: 3.2.1.qualifier
 Bundle-SymbolicName: com.rockwellcollins.atc.agree.ui; singleton:=true
 Bundle-ActivationPolicy: lazy
 Require-Bundle: com.rockwellcollins.atc.agree;bundle-version="[3.1.0,4.0.0)";visibility:=reexport,
- org.eclipse.xtext.ui;bundle-version="[2.25.0,3.0.0)",
- org.eclipse.ui.editors;bundle-version="[3.5.0,4.0.0)",
  org.eclipse.ui.ide;bundle-version="[3.5.0,4.0.0)",
  org.eclipse.xtext.ui.shared;bundle-version="[2.25.0,3.0.0)",
- org.eclipse.ui;bundle-version="[3.119.0,4.0.0)",
- org.eclipse.xtext.builder;bundle-version="[2.25.0,3.0.0)",
- org.antlr.runtime;bundle-version="[3.2.0,3.2.1)",
- org.eclipse.xtext.common.types.ui;bundle-version="[2.25.0,3.0.0)",
  org.eclipse.compare;bundle-version="[3.7.0,4.0.0)",
- org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)",
- org.osate.xtext.aadl2.properties.ui;bundle-version="[4.0.0,5.0.0)",
  org.osate.aadl2;bundle-version="[5.0.0,6.0.0)",
- org.osate.aadl2.modelsupport;bundle-version="[7.0.0,8.0.0)",
  org.osate.annexsupport;bundle-version="[4.0.1,5.0.0)",
  org.osate.xtext.aadl2.ui;bundle-version="[7.0.0,8.0.0)",
- org.eclipse.xtext.xbase.lib;bundle-version="[2.14.0,3.0.0)",
- org.eclipse.xtend.lib;bundle-version="[2.25.0,3.0.0)";resolution:=optional,
  org.eclipse.xtext.ui.codetemplates.ui;bundle-version="[2.25.0,3.0.0)"
-Import-Package: org.apache.log4j;version="[1.1.0,2.0.0)",
- org.eclipse.xtext.xbase.lib;version="[2.25.0,3.0.0)",
- org.osate.ui.wizards
+Import-Package: org.apache.log4j;version="[1.1.0,2.0.0)"
 Bundle-RequiredExecutionEnvironment: JavaSE-17
 Export-Package: com.rockwellcollins.atc.agree.parsing;version="3.2.1",
  com.rockwellcollins.atc.agree.ui.contentassist;version="3.2.1",

com.rockwellcollins.atc.agree/META-INF/MANIFEST.MF

@@ -5,24 +5,12 @@ Bundle-Vendor: Rockwell Collins, Inc.
 Bundle-Version: 3.1.1.qualifier
 Bundle-SymbolicName: com.rockwellcollins.atc.agree; singleton:=true
 Bundle-ActivationPolicy: lazy
-Require-Bundle: org.eclipse.xtext;bundle-version="[2.25.0,3.0.0)";visibility:=reexport,
- org.eclipse.xtext.xbase;bundle-version="[2.25.0,3.0.0)";resolution:=optional;visibility:=reexport,
- org.eclipse.xtext.generator;bundle-version="[2.25.0,3.0.0)";resolution:=optional,
- org.apache.commons.logging;bundle-version="[1.0.4,2.0.0)";resolution:=optional,
- org.eclipse.emf.codegen.ecore;bundle-version="[2.25.0,3.0.0)";resolution:=optional,
- org.eclipse.emf.mwe.utils;bundle-version="[1.6.0,2.0.0)";resolution:=optional,
+Require-Bundle: org.eclipse.xtext.generator;bundle-version="[2.25.0,3.0.0)";resolution:=optional,
  org.eclipse.emf.mwe2.launch;bundle-version="[2.12.0,3.0.0)";resolution:=optional,
  org.osate.aadl2;bundle-version="[5.0.0,6.0.0)",
  org.osate.xtext.aadl2;bundle-version="[7.0.0,8.0.0)",
  org.osate.xtext.aadl2.properties;bundle-version="[3.0.0,4.0.0)",
- org.eclipse.xtext.util;bundle-version="[2.25.0,3.0.0)",
- org.eclipse.emf.ecore;bundle-version="[2.22.0,3.0.0)",
- org.eclipse.emf.common;bundle-version="[2.22.0,3.0.0)",
- org.antlr.runtime;bundle-version="[3.2.0,3.2.1)",
- org.eclipse.xtext.common.types;bundle-version="[2.25.0,3.0.0)",
- org.osate.annexsupport;bundle-version="[4.0.1,5.0.0)",
- org.eclipse.xtext.xbase.lib;bundle-version="[2.14.0,3.0.0)"
-Import-Package: org.apache.log4j;version="[1.2.0,2.0.0)"
+ org.osate.annexsupport;bundle-version="[4.0.1,5.0.0)"
 Bundle-RequiredExecutionEnvironment: JavaSE-17
 Export-Package: com.rockwellcollins.atc.agree;version="3.1.1",
  com.rockwellcollins.atc.agree.services;version="3.1.1",