Home

Welcome to your wiki!

This is the default page, edit it as you see fit. To add a new page simply reference it within brackets, e.g.: [SamplePage].

The wiki uses Markdown syntax.

Project Admins:

• Chihhong Cheng

[Chihhong Cheng]

Update within ver 1.0 rev1:

1. Modify the example in /Ptolemy folder to include one that can be directly simulated with Ptolemy II.

2. Modify the internal data structure to generate the same controller (in textural format), given a particular specification.

[Chihhong Cheng]

Update within ver 1.0 rev2:

Basic code cleaning.

[Chihhong Cheng]

Update within ver 1.0 rev3:

1. Modify the output strategy format (Ptolemy II template), so that multiple guard conditions can be merged using BDD. E.g., conditions like (a==false || a==true) will be changed to a_isPresent.

2. Modify the Buechi game engine to perform a reachability analysis after the strategy is generated. This allows to prune out states in a strategy that are never visited.

Todo in rev4: Allow to generate strategies with smaller set of states.

[Chihhong Cheng]

GPL version_1.05:

1. Support of IEC 61131-3 Structured Text
2. New examples, refined tutorials
3. License change (old version are BSD-based; new versions are GPL-based)

[Chihhong Cheng]

Update GPL-version 1.05.1

(a) Fix the problem of using timers due to two reasons. For CODESYS structured text (ST), the triggering of timers can not be locating inside an IF statement (although it is syntacally OK, in execution the timer is surprisingly not enabled). Therefore, one needs to move it out from control loop.

Also, the semantic of timer is different from what is presented in CAV paper. In CAV paper, we use t.start as a Boolean variable to start the timer, and when t.expire turns true, we know that the time has elapsed. In actual implementation, the start of timer needs to be triggered over a rising edge. Also, one needs to continuously set IN to be true, in order to elapse the time. Therefore, we need to introduce additional variables to wrap timer TON such that it matches the way how we describe the timer (t.start for enabling; t.expire for expiration)

The fix is to introduce in the implementation, apart from t_start (the one where controller triggers), additional variables t_up (for generating rising edge) and t_reset (the one to be continuously feed into IN as TRUE). By doing so, we move the triggering of timer outside the state machine.

By doing so, there exists one period (normally it is 100ms) difference for the timer. One can decide if it is acceptable. If not, then one should adjust the timer constant by subtracting one period.

(b) Improve the process of assumption generation. Originally the synthesized assumptions, when combined with original assumption, can smartly make the overall assumption FALSE, thereby easily creating a controller. However, this is in general not the thing which a designer wants. Therefore, in the implementation we have added a testing step to ensure that this will not happen.

(c) Add explicit warning such that the use of timers is only associated with output format ST

[Chihhong Cheng]

Update GPL-version 1.05.2

Although G4LTL-ST faithfully creates controllers from logic specifications, if the provided spec is wrong, then the synthesized controller is useless. Therefore, for examples in examples\Example_IndustrialAutomation, a careful examination and polishing of specification is being executed, where we place each synthesized controller to the simulation environment to observe if the generated behavior reflects the designer intention. If not, then we polish the specification to achieve the goal.

[Chihhong Cheng]

Update GPL-version 1.05.3

Create CODESYS projects for nearly all examples in examples\Example_IndustrialAutomation, and attach a Modbus TCP I/O to support interactive simulation. All implementations follow the orally specified behavior.

[Chihhong Cheng]

Update GPL-version 1.5.4

1. Updated tutorial for section 2 (specification and implementation methodology)
2. Provided an industrial I/O simulator based on Modbus TCP.
3. All 14 examples in examples\Example_IndustrialAutomation are tested for "correctness of specification" using PLC simulation.
4. Provide instructions how to resolve problems related to CODESYS project versioning.

[Chihhong Cheng]

Update GPL-version 1.06

Change the code generation template for Structured Text, such that it is more efficient for relatively complex examples.

[Chihhong Cheng]

Update GPL-version 1.07

1. Change the variable ordering in BDD for composing partial strategies, such that extracting the state information can be easier (by taking directly a substring)
2. Slightly restructure the package
3. Change Tutorial.txt