Index of /ptolemyII/ptII10.0/ptII10.0.1/ptolemy/vergil/basic/imprt/g4ltl

Name	Last modified	Size

Parent Directory		-
demo/	2014-11-21 16:02	-
test/	2014-10-22 21:16	-
package.html	2013-04-25 14:59	488
G4LTL.gif	2013-03-08 06:44	1.6K
makefile	2013-04-25 14:59	2.3K
G4LTL.class	2014-12-16 13:44	3.1K
ImportG4LTLAction.class	2014-12-16 13:44	5.7K
G4LTL.java	2014-10-22 17:52	7.1K
ImportG4LTLAction.java	2014-10-22 17:52	9.8K
g4ltl.jar	2014-12-16 13:44	11K

Automatic FSMActor Synthesis

FSMActor synthesis from specifications

This is an attempt that tries to equip Ptolemy II with novel abilities to automatically synthesize controllers from high-level specifications. The underlying synthesis engine is based on a modified (without GUI) version of G4LTL, a research tool developed by fortiss GmbH (An-Institut Technische Universität München).

Methodology

The synthesis methodology follows concepts within (1) signals and systems and (2) actor-oriented programming, where a controller takes input tokens and produces subsequently output tokens. The synthesized controller is a Mealy machine.

Instructions	Example
Specify input and output variables.	## Use two inputs and two outputs INPUT req1, req2 OUTPUT grant1, grant2
1. Specify the desired behavior of the controller as a formula using logical operators, temporal operators, and connect subformulas with appropriate parentheses. Logical operators: use "\|\|", "&&", "!" , "->" for logical or, and, not, and imply. Temporal operators (let A, B be subformulas): Use "ALWAYS (A)" to specify that the scenario A always holds Use "EVENTUALLY (A)" to specify that the scenario A eventually holds Use "NEXT (A)" to specify that in the next round, scenario A holds Use "A UNTIL B" to specify that A holds until B holds 2. Every line in the specification is connected with && implicitly. 3. A line starting with ASSUME means the assumptions posed on the environment. Originally, in the synthesis framework, the input is uncontrollable. Using ASSUME allows to constrain unreasonable scenarios that the environment never produces.	## whenever the received input req1 is true, the produced token of grant1 should be true ALWAYS (req1 -> grant1) ## whenever req1 is true, the next produced token of grant1 should be true ALWAYS (req1 -> NEXT grant1) ## whenever req1 is true, eventually the controller should produce grant1 that is also true ALWAYS (req1 -> EVENTUALLY grant1)
Invoke the synthesis engine to generate a correct controller.

Demonstrations

Demo 1: Simple arbitor
Demo 2: Arbitor with guaranteed service for a super client
Demo 3: Controller with error handling
Demo 4: Controllers with numerical conditions

Demo 1: Simple arbitor

In this demo, we illustrate how to automatically create an FSMActor from specification.

Open $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/Arbitor/Arbitor.xml
On the menu bar, select "File -> Import -> Import FSMActor using synthesis"
A dialog box will appear, asking you to provide the specification. The specification describes "what" should a controller do without detailing how such controller is implemented. It is located at $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/Arbitor/ArbitorLTL.txt
One can select synthesis techniques between Co-Buechi and Buechi solvers. Here we try Co-Buchi (both solvers work). Select the unroll depth to be "1". Higher unroll depth enables to explore more possibilities in strategy finding. However the synthesis time will also take longer.
The synthesized FSMActor named "model" now appears on the screen. To perform simulation, create links between ports.

[Feed input to FSMActor] Link the output of Client1 to the port req1 in model, and similarly, link the output of Client2 to the port req2 in model.
[Produce output from FSMActor] Link model.grant1 to the output screen Grant1, and model.grant2 to the output screen Grant2.

The model is fully connected and can be executed with simulation.

Demo 2: Arbitor with guaranteed service for a super-client

In this demo, we illustrate how to automatically create an arbitor which set explicit guarantees for the super-client.

Open $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/PriorityArbitor/PriorityArbitor.xml
On the menu bar, select "File -> Import -> Import FSMActor using synthesis"
A dialog box will appear, asking you to provide the specification. The specification describes "what" should a controller do without detailing how such controller is implemented. It is located at $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/PriorityArbitor/PriorityArbitorLTL.txt
One can select synthesis techniques between Co-Buechi and Buechi solvers. Here we try Co-Buchi (both solvers work). Select the unroll depth to be "3". In this example, using unroll depth 1 is not sufficient to find a controller.
The synthesized FSMActor named "model" now appears on the screen. To perform simulation, create links between ports.

[Feed input to FSMActor] Link the output of ImportantClient1 to the port req1 in model, and similarly, link the output of Client2 / Client3 to the port req2 / req3 in model.
[Produce output from FSMActor] Link port grant1 / grant2 / grant3 to the output screen Grant1 / Grant2 / Grant3.

The model is fully connected and can be executed with simulation.

Demo 3: Controller with error handling

In this example, we illustrate how to automatically create an arbitor that allows to suspend itself when encountering errors.

Open $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/ErrorHandling/ErrorHandling.xml
On the menu bar, select "File -> Import -> Import FSMActor using synthesis"
A dialog box will appear, asking you to provide the specification. The specification describes "what" should a controller do without detailing how such controller is implemented. It is located at $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/ErrorHandling/ErrorHandlingLTL.txt
One can select synthesis techniques between Co-Buechi and Buechi solvers. Here we try Co-Buchi (both solvers work). Select the unroll depth to be "3". In this example, using unroll depth 1 is not sufficient to find a controller.
The synthesized FSMActor named "model" now appears on the screen. To perform simulation, create links between ports.

[Feed input to FSMActor] Link the output of SetVariable(V_err) / SetVariable2(V_oper) / SetVariable7(V_req1) / SetVariable6(V_req2) to the port error/operator/req1/req2 in model.
[Produce output from FSMActor] Link port grant1 / grant2 / stop to the input of SetVariable3 / SetVariable4 / SetVariable5.

The model is fully connected and can be executed with simulation.

Demo 4: Numerical conditions

In this example, we illustrate how can FSMActor synthesis be extended with non-Boolean inputs. Please follow the instruction in the model $PTII/ptolemy/vergil/basic/imprt/g4ltl/demo/Numerical/Numerical.xml