![]() | Name | Last modified | Size | Description |
---|---|---|---|---|
![]() | Parent Directory | - | ||
![]() | g4ltl.jar | 2014-12-16 13:44 | 11K | |
![]() | ImportG4LTLAction.java | 2014-10-22 17:52 | 9.8K | |
![]() | G4LTL.java | 2014-10-22 17:52 | 7.1K | |
![]() | ImportG4LTLAction.class | 2014-12-16 13:44 | 5.7K | |
![]() | G4LTL.class | 2014-12-16 13:44 | 3.1K | |
![]() | makefile | 2013-04-25 14:59 | 2.3K | |
![]() | G4LTL.gif | 2013-03-08 06:44 | 1.6K | |
![]() | package.html | 2013-04-25 14:59 | 488 | |
![]() | test/ | 2014-10-22 21:16 | - | |
![]() | demo/ | 2014-11-21 16:02 | - | |
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.
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. |
In this demo, we illustrate how to automatically create an arbitor which set explicit guarantees for the super-client.
In this example, we illustrate how to automatically create an arbitor that allows to suspend itself when encountering errors.
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