Annotations

org.javabip.api/pom.xml

@@ -1,8 +1,25 @@
 <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>
+    <dependencies>
+        <dependency>
+            <groupId>org.openjfx</groupId>
+            <artifactId>javafx-base</artifactId>
+            <version>17-ea+11</version>
+        </dependency>
+        <dependency>
+            <groupId>org.antlr</groupId>
+            <artifactId>antlr4-runtime</artifactId>
+            <version>4.8-1</version>
+            <scope>compile</scope>
+        </dependency>
+        <dependency>
+            <groupId>junit</groupId>
+            <artifactId>junit</artifactId>
+        </dependency>
+    </dependencies>
 
-	<parent> 
+    <parent>
 		<groupId>org.javabip</groupId>
 		<artifactId>org.javabip.parent</artifactId>
 		<version>0.1.0-SNAPSHOT</version>
@@ -51,8 +68,8 @@
 				<groupId>org.apache.maven.plugins</groupId>
 				<artifactId>maven-compiler-plugin</artifactId>
 				<configuration>
-					<source>1.6</source>
-					<target>1.6</target>
+					<source>8</source>
+					<target>8</target>
 				</configuration>
 			</plugin>
 		</plugins>

org.javabip.api/src/main/java/org/javabip/annotations/Invariant.java

@@ -0,0 +1,38 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Larisa Safina, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 23.02.22
+ */
+
+package org.javabip.annotations;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+/**
+ * An invariant annotation, which specifies the invariant of a component
+ */
+@Retention(RetentionPolicy.RUNTIME)
+public @interface Invariant {
+
+	/**
+	 * expr is a string containing plain Java expressions
+	 * it must hold after construction of the component, can be assumed to hold before a transition, and must hold after a transition
+	 * @return value
+	 */
+	String value();
+}

org.javabip.api/src/main/java/org/javabip/annotations/Pure.java

@@ -0,0 +1,30 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Larisa Safina, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 23.02.22
+ */
+
+package org.javabip.annotations;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+/**
+ * An pure annotation indicates that the method is a side-effect free heap-dependent method
+ */
+@Retention(RetentionPolicy.RUNTIME)
+public @interface Pure {}

org.javabip.api/src/main/java/org/javabip/annotations/StatePredicate.java

@@ -0,0 +1,45 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Larisa Safina, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 23.02.22
+ */
+
+package org.javabip.annotations;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+/**
+ * A state predicate annotation
+ */
+@Retention(RetentionPolicy.RUNTIME)
+public @interface StatePredicate {
+
+	/**
+	 * state is a string containing the name of the state
+	 * @return the name of the state.
+	 */
+	String state();
+
+	/**
+	 * expr is a string containing plain Java expressions
+	 * it must hold when the state is entered.
+	 * when the component moves to a new state, expr may be assumed to hold at the start of the transition
+	 * @return expr.
+	 */
+	String expr();
+}

org.javabip.api/src/main/java/org/javabip/annotations/StatePredicates.java

@@ -0,0 +1,39 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, Alina Zolotukhina and Larisa Safina
+ * Date: 22.03.22
+ */
+
+package org.javabip.annotations;
+
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+
+/**
+ * It makes it possible to assign multiple state predicates within one function.
+ *
+ */
+@Retention(RetentionPolicy.RUNTIME)
+public @interface StatePredicates {
+
+	/**
+	 * It returns the array of transitions.
+	 * 
+	 * @return array of transitions.
+	 */
+	StatePredicate[] value();
+}

org.javabip.api/src/main/java/org/javabip/annotations/Transition.java

@@ -14,8 +14,8 @@
  * See the License for the specific language governing permissions and
  * limitations under the License.
  *
- * Author: Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek and Alina Zolotukhina
- * Date: 15.10.12
+ * Author: Simon Bliudze, Anastasia Mavridou, Larisa Safina, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 23.02.22
  */
 
 package org.javabip.annotations;
@@ -59,4 +59,18 @@
 	 */
 	String guard() default "";
 
+	/**
+	 * pre condition that is supposed to hold before the execution of the update function
+	 * can be useful to check properties specific to a transition, which you don’t want to put in a state predicate or component invariant
+	 * @return pre condition
+	 */
+	String pre() default "";
+
+	/**
+	 * post condition that is supposed to hold after the execution of the update function
+	 * can be useful to check properties specific to a transition, which you don’t want to put in a state predicate or component invariant
+	 * @return post condition
+	 */
+	String post() default "";
+
 }

org.javabip.api/src/main/java/org/javabip/api/BIPActor.java

@@ -44,4 +44,9 @@ public interface BIPActor {
 	 */
 	void inform(String portID, Map<String, Object> data);
 
+	/**
+	 * It returns the control state of the BIP component that Executor runs.
+	 */
+	String getState ();
+
 }

org.javabip.api/src/main/java/org/javabip/api/BIPEngine.java

@@ -80,6 +80,22 @@ public interface BIPEngine {
 	void informSpecific(BIPComponent decidingComponent, Port decidingPort,
 			Map<BIPComponent, Set<Port>> disabledCombinations);
 
+	/**
+	 * informInternal is served for notifying the engine on the internal transition happened on the component
+	 * needed for the monitoring
+	 * @param decidingComponent
+	 * @param currentState
+	 */
+	void informInteral(BIPComponent decidingComponent, String currentState);
+
+	/**
+	 * informSpontaneous is served for notifying the engine on the spontaneous transition happened on the component
+	 * needed for the monitoring
+	 * @param decidingComponent
+	 * @param currentState
+	 */
+	void informSpontaneous(BIPComponent decidingComponent, String currentState);
+
 	/**
 	 * It starts the BIP engine thread.
 	 */

org.javabip.api/src/main/java/org/javabip/api/DataWire.java

@@ -39,6 +39,13 @@ public interface DataWire {
 	 */
 	public PortBase getTo();
 
+	/**
+	 * Gets the port to which the data is being sent to.
+	 *
+	 * @return the port to which the data is being sent to.
+	 */
+	public Boolean isCopy();
+
 	/**
 	 * Checks if the given input data of the given component type is at the incoming end of the wire. The function is
 	 * used by the BIP Engine.

org.javabip.api/src/main/java/org/javabip/api/ExecutableBehaviour.java

@@ -20,14 +20,15 @@
 
 package org.javabip.api;
 
+import javafx.util.Pair;
+import org.javabip.exceptions.BIPException;
+
 import java.lang.invoke.MethodHandle;
 import java.lang.reflect.InvocationTargetException;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
 
-import org.javabip.exceptions.BIPException;
-
 /**
  * It provides an executable behavior that makes it possible to execute transitions within the behavior.
  */
@@ -171,4 +172,10 @@ public boolean existInCurrentStateAndEnabledEnforceableWithoutData(Map<String, B
 	 * @return the map between guard names and their boolean values.
 	 */
 	public Map<String, Boolean> computeGuardsWithoutData(String currentState);
-}
+
+	Pair<Boolean, String> checkInvariant() throws BIPException;
+
+	Pair<Boolean, String> checkTransitionCondition(Object transition, Boolean pre);
+
+	Pair<Boolean, String> checkStatePredicate(String currentState);
+}

org.javabip.api/src/main/java/org/javabip/api/Invariant.java

@@ -0,0 +1,34 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Larisa Safina, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 23.02.22
+ */
+
+package org.javabip.api;
+
+/**
+ * It specifies the interface for class invariant
+ */
+public interface Invariant {
+
+	/**
+	 * @return the invariant expression
+	 */
+	String expression();
+
+	boolean evaluateInvariant(Class<?> componentClass, Object bipComponent);
+}

org.javabip.api/src/main/java/org/javabip/api/Pure.java

@@ -0,0 +1,26 @@
+/*
+ * Copyright 2012-2016 École polytechnique fédérale de Lausanne (EPFL), Switzerland
+ * Copyright 2012-2016 Crossing-Tech SA, Switzerland
+ * 
+ * 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.
+ *
+ * Author: Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek and Alina Zolotukhina
+ * Date: 15.10.12
+ */
+
+package org.javabip.api;
+
+/**
+ * It specifies the interface for pure annotation
+ */
+public interface Pure { }