Headless agree

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

@@ -14,8 +14,8 @@ Require-Bundle: org.eclipse.ui;bundle-version="[3.119.0,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.0.0,4.0.0)",
- com.rockwellcollins.atc.agree.ui;bundle-version="[3.1.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)",

com.rockwellcollins.atc.agree.analysis/src/com/rockwellcollins/atc/agree/analysis/preferences/PreferenceInitializer.java

@@ -34,7 +34,9 @@ public void initializeDefaultPreferences() {
 		IPreferenceStore store = Activator.getDefault().getPreferenceStore();
 		store.setDefault(PreferenceConstants.PREF_MODEL_CHECKER, PreferenceConstants.MODEL_CHECKER_JKIND);
 		store.setDefault(PreferenceConstants.PREF_SOLVER, PreferenceConstants.SOLVER_SMTINTERPOL);
+		store.setDefault(PreferenceConstants.PREF_NO_KINDUCTION, false);
 		store.setDefault(PreferenceConstants.PREF_INDUCT_CEX, true);
+		store.setDefault(PreferenceConstants.PREF_SUPPORT, false);
 		store.setDefault(PreferenceConstants.PREF_SMOOTH_CEX, false);
 		store.setDefault(PreferenceConstants.PREF_UNSPECIFIED_AADL_PROPERTIES, false);
 		store.setDefault(PreferenceConstants.PREF_DISPLAY_DECIMAL_CEX, false);

com.rockwellcollins.atc.agree.cli/.classpath

@@ -0,0 +1,9 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+	<classpathentry exported="true" kind="lib" path="lib/commons-cli.jar"/>
+	<classpathentry exported="true" kind="lib" path="lib/gson.jar"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17"/>
+	<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
+	<classpathentry kind="src" path="src"/>
+	<classpathentry kind="output" path="bin"/>
+</classpath>

com.rockwellcollins.atc.agree.cli/.gitignore

@@ -0,0 +1,3 @@
+/bin/
+/lib/
+/target/

com.rockwellcollins.atc.agree.cli/.project

@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>com.rockwellcollins.atc.agree.cli</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.jdt.core.javabuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
+			<name>org.eclipse.pde.ManifestBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
+			<name>org.eclipse.pde.SchemaBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.pde.PluginNature</nature>
+		<nature>org.eclipse.jdt.core.javanature</nature>
+	</natures>
+</projectDescription>

com.rockwellcollins.atc.agree.cli/.settings/org.eclipse.jdt.core.prefs

@@ -0,0 +1,9 @@
+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
+org.eclipse.jdt.core.compiler.compliance=17
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
+org.eclipse.jdt.core.compiler.release=enabled
+org.eclipse.jdt.core.compiler.source=17

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

@@ -0,0 +1,25 @@
+Manifest-Version: 1.0
+Bundle-ManifestVersion: 2
+Bundle-Name: Cli
+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,
+ com.rockwellcollins.atc.agree,
+ org.osate.aadl2,
+ org.osate.pluginsupport,
+ org.osate.aadl2.instantiation,
+ com.collins.trustedsystems.jkindapi,
+ com.rockwellcollins.atc.agree.analysis,
+ org.osate.annexsupport
+Bundle-RequiredExecutionEnvironment: JavaSE-17
+Automatic-Module-Name: com.rockwellcollins.atc.agree.cli
+Bundle-ActivationPolicy: lazy
+Bundle-ClassPath: lib/commons-cli.jar,
+ lib/gson.jar,
+ .

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

@@ -0,0 +1,40 @@
+# Running AGREE from the command line
+
+AGREE can be run from the command line.  All AGREE tool preferences, along with other run options can be specified as command line arguments.  Usage is as follows:
+
+| Argument | Description |  
+|---|---|  
+| -analyzeUnspecifiedAADLProperties  | optional, analyze unspecified AADL properties |  
+| -application <arg>                 | required, the name of this analysis (com.rockwellcollins.atc.agree.cli.Agree) |  
+| -c,--compImpl <arg>                | required, qualified component implementation name |  
+| -consistencyDepth <arg>            | optional, consistency depth, default 1 | 
+| -data <arg>                        | required, path of workspace | 
+| -disableKInduction                 | optional, disable k-induction | 
+| -displayCounterexamplesAsDecimal   | optional, display counterexamples as decimal | 
+| -f,--files <arg>                   | optional, supplementary AADL files (absolute paths) | 
+| -generateBlamedCounterexamples     | optional, generate blamed counterexamples |
+| -generateSmoothCounterexamples     | optional, generate smooth counterexamples | 
+| -getSetOfSupport                   | optional, get set of support | 
+| -h,--help                          | print this message | 
+| -m,--modelChecker <arg>            | optional, model checker, default JKind | 
+| -maxInductionDepth <arg>           | optional, maximum induction depth, default 200 | 
+| -maxPDRInstances <arg>             | optional, maximum number of PDR instances, default 0 | 
+| -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) | 
+| -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 | 
+| -v,--validationOnly                | validation only, default false | 
+| -w,--exitOnValidtionWarning        | exit on validation warning, default false | 
+
+# 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:
+
+`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.

com.rockwellcollins.atc.agree.cli/build.properties

@@ -0,0 +1,7 @@
+source.. = src/
+bin.includes = META-INF/,\
+               .,\
+               plugin.xml,\
+               lib/gson.jar,\
+               lib/commons-cli.jar
+

com.rockwellcollins.atc.agree.cli/plugin.xml

@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<?eclipse version="3.4"?>
+<plugin>
+   <extension
+         id="Agree"
+         name="Headless Agree"
+         point="org.eclipse.core.runtime.applications">
+         <application
+            cardinality="singleton-global"
+            thread="main"
+            visible="true">
+         <run
+               class="com.rockwellcollins.atc.agree.cli.Agree">
+         </run>
+      </application>
+   </extension>
+
+</plugin>

com.rockwellcollins.atc.agree.cli/pom.xml

@@ -0,0 +1,116 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+  <modelVersion>4.0.0</modelVersion>
+  <parent>
+    <groupId>com.rockwellcollins.atc.agree</groupId>
+    <artifactId>com.rockwellcollins.atc.agree.parent</artifactId>
+    <version>2.10.1-SNAPSHOT</version>
+  </parent>
+  <artifactId>com.rockwellcollins.atc.agree.cli</artifactId>
+  <version>1.0.1-SNAPSHOT</version>
+  <packaging>eclipse-plugin</packaging>
+  <properties>
+		<commons-cli.version>1.5.0</commons-cli.version>
+		<gson.version>2.8.9</gson.version>
+	</properties>
+
+	<build>
+		<plugins>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-dependency-plugin</artifactId>
+				<version>3.2.0</version>
+				<executions>
+					<execution>
+						<id>copy-dependencies</id>
+						<phase>initialize</phase>
+						<goals>
+							<goal>copy</goal>
+						</goals>
+						<configuration>
+							<artifactItems>
+								<artifactItem>
+									<groupId>com.google.code.gson</groupId>
+									<artifactId>gson</artifactId>
+									<version>${gson.version}</version>
+								</artifactItem>
+								<artifactItem>
+									<groupId>commons-cli</groupId>
+									<artifactId>commons-cli</artifactId>
+									<version>${commons-cli.version}</version>
+								</artifactItem>
+							</artifactItems>
+							<outputDirectory>lib</outputDirectory>
+							<stripVersion>true</stripVersion>
+							<overWriteReleases>true</overWriteReleases>
+							<overWriteSnapshots>true</overWriteSnapshots>
+						</configuration>
+					</execution>
+				</executions>
+			</plugin>
+		</plugins>
+		<pluginManagement>
+			<plugins>
+				<plugin>
+					<groupId>org.apache.maven.plugins</groupId>
+					<artifactId>maven-clean-plugin</artifactId>
+					<version>2.5</version>
+					<configuration>
+						<filesets>
+							<fileset>
+								<directory>${basedir}/lib</directory>
+								<includes>
+									<include>**/*</include>
+								</includes>
+							</fileset>
+						</filesets>
+					</configuration>
+				</plugin>
+				<plugin>
+					<groupId>org.eclipse.m2e</groupId>
+					<artifactId>lifecycle-mapping</artifactId>
+					<version>1.0.0</version>
+					<configuration>
+						<lifecycleMappingMetadata>
+							<pluginExecutions>
+								<pluginExecution>
+									<pluginExecutionFilter>
+										<groupId>
+											org.apache.maven.plugins
+										</groupId>
+										<artifactId>
+											maven-dependency-plugin
+										</artifactId>
+										<versionRange>
+											[3.0.0,)
+										</versionRange>
+										<goals>
+											<goal>copy</goal>
+										</goals>
+									</pluginExecutionFilter>
+									<action>
+										<ignore />
+									</action>
+								</pluginExecution>
+							</pluginExecutions>
+						</lifecycleMappingMetadata>
+					</configuration>
+				</plugin>
+			</plugins>
+		</pluginManagement>
+	</build>
+
+	<dependencies>
+		<!-- https://mvnrepository.com/artifact/com.google/gson -->
+		<dependency>
+			<groupId>commons-cli</groupId>
+			<artifactId>commons-cli</artifactId>
+			<version>${commons-cli.version}</version>
+		</dependency>
+		<dependency>
+			<groupId>com.google.code.gson</groupId>
+			<artifactId>gson</artifactId>
+			<version>${gson.version}</version>
+		</dependency>
+	</dependencies>
+</project>

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

@@ -0,0 +1,42 @@
+package com.rockwellcollins.atc.agree.cli;
+
+import org.eclipse.osgi.service.environment.EnvironmentInfo;
+import org.eclipse.ui.plugin.AbstractUIPlugin;
+import org.osgi.framework.BundleContext;
+import org.osgi.framework.ServiceReference;
+
+
+//public class Activator implements BundleActivator {
+public class Activator extends AbstractUIPlugin {
+
+	private static BundleContext context;
+
+	// The shared instance
+	private static Activator plugin;
+
+	static BundleContext getContext() {
+		return context;
+	}
+
+	@Override
+	public void start(BundleContext bundleContext) throws Exception {
+		Activator.context = bundleContext;
+		plugin = this;
+	}
+
+	@Override
+	public void stop(BundleContext bundleContext) throws Exception {
+		Activator.context = null;
+		plugin = null;
+	}
+
+	/**
+	 * Returns the shared instance
+	 *
+	 * @return the shared instance
+	 */
+	public static Activator getDefault() {
+		return plugin;
+	}
+
+}