Tutorial 2 - csp
Last modified by Richard Kreissig on 2023/09/07 09:50
T2A1
- Extended SCCharts are merely syntactic sugar to Core SCCharts. Each Extended SCChart is expressable in Core SCChart syntax.
- Compilation of code from a Core SCChart is much simpler than compiling an extended SCChart. Because of the semantically equality, it's much easier to perform a model-to-model transformation than to compile an extended SCChart.
- A basic block is a set of instructions, that can be executed as one piece. Instructions with more than one incoming or outgoing sequential control-flow-edges or tick edges trigger a break between basic blocks.
- The ordering of a schedule is influenced by data-dependencies such as write-read, abs.write-rel.write and by the sequential control-flow.
T2A2
Created:
Received:
T2A4
Extended features:
- Count Delay: Wait 5 seconds.
Transformation: External counter. Reset in entry action. Count in during action. During action in parent state here because of empty complex state "stop".
The entry action to reset the counter is missing in the automatic transformation. I added the entry action manually and removed the unnecessary initialization of the counter. - During: Action during a state is active.
Transformation: Parallel regions. First increments the counter until the other one finishes. - Entry: Action on entering a state.
Transformation: Additional init-state with immediate transition and the same label the entry action had.
Core SCChart:
Normalize:
- Trigger and Effect: Split Trigger and Effects in sequential (immediate) transitions.
- Surface Depth: States with outgoing non-immediate transitions must only have one outgoing transition.
SCG:
Write-write-conflicts may occur while accessing the track-variable. These are between the initialization of the track and lowering the speed or stopping the train when it enters the station again. Thus these conflict can be easily resolved by sequentializing the initialization and the rest of the controller.
Futhermore there exists a dependency-cycle between the increment and read of the counter-variable and the write and read of the _term-variable. Therefore the SCG is not ASC-schedulable. This can be fixed by sequentialising the counter. We know the counter has to wait 5 seconds. So the counter can be modeled in form of 5 sequential states.
T2A5
Explanation of Changes see above.
Generated SCG has no dependencies:
Generated c code:
Generated c Code
/*****************************************************************************/
/* G E N E R A T E D C C O D E */
/*****************************************************************************/
/* KIELER - Kiel Integrated Environment for Layout Eclipse RichClient */
/* */
/* http://www.informatik.uni-kiel.de/rtsys/kieler/ */
/* Copyright 2014 by */
/* + Christian-Albrechts-University of Kiel */
/* + Department of Computer Science */
/* + Real-Time and Embedded Systems Group */
/* */
/* This code is provided under the terms of the Eclipse Public License (EPL).*/
/*****************************************************************************/
int second ;;
int contact0 ;;
int contact1 ;;
int track ;;
int _GO ;;
int guard21_e1 ;;
int guard21_e1 ;;
int guard22_e1 ;;
int guard0 ;;
int guard1 ;;
int guard2 ;;
int guard3 ;;
int guard4 ;;
int guard5 ;;
int guard6 ;
int PRE_guard6 ;;
int guard7 ;;
int guard8 ;
int PRE_guard8 ;;
int guard9 ;;
int guard10 ;
int PRE_guard10 ;;
int guard11 ;;
int guard12 ;
int PRE_guard12 ;;
int guard13 ;;
int guard14 ;
int PRE_guard14 ;;
int guard15 ;;
int guard16 ;;
int guard17 ;
int PRE_guard17 ;;
int guard18 ;;
int guard19 ;
int PRE_guard19 ;;
int guard20 ;;
int guard21 ;;
int guard22 ;;
int guard23 ;
int reset(){
_GO = 1;
}
int tick(){
guard0 = _GO;
Tick: {
if (guard1) {
track = 60;
}
guard2 = guard1;
guard15 = (PRE_guard14)
;
guard16 = (
guard15 &&
second
)
;
if (guard16) {
track = 60;
}
guard3 = (
guard2 ||
guard16
)
;
guard20 = (PRE_guard19)
;
guard4 = (
(
guard3 &&
contact0
) ||
(
guard20 &&
contact0
)
)
;
if (guard4) {
track = 20;
}
guard18 = (PRE_guard17)
;
guard5 = (
(
guard4 &&
contact1
) ||
(
guard18 &&
contact1
)
)
;
if (guard5) {
track = 0;
}
guard7 = (PRE_guard6)
;
guard6 = (
guard5 ||
(
guard7 &&
(!(second))
)
)
;
guard9 = (PRE_guard8)
;
guard8 = (
(
guard7 &&
second
) ||
(
guard9 &&
(!(second))
)
)
;
guard11 = (PRE_guard10)
;
guard10 = (
(
guard9 &&
second
) ||
(
guard11 &&
(!(second))
)
)
;
guard13 = (PRE_guard12)
;
guard12 = (
(
guard11 &&
second
) ||
(
guard13 &&
(!(second))
)
)
;
guard14 = (
(
guard13 &&
second
) ||
(
guard15 &&
(!(second))
)
)
;
guard17 = (
(
guard4 &&
(!(contact1))
) ||
(
guard18 &&
(!(contact1))
)
)
;
guard19 = (
(
guard3 &&
(!(contact0))
) ||
(
guard20 &&
(!(contact0))
)
)
;
guard21 = 0;
guard21_e1 = (!((
guard19 ||
(
guard17 ||
(
guard6 ||
(
guard8 ||
(
guard10 ||
(
guard12 ||
guard14
)
)
)
)
)
)
))
;
guard22 = (
(
guard21_e1 ||
guard21
) &&
guard21
)
;
guard22_e1 = (!((
guard19 ||
(
guard17 ||
(
guard6 ||
(
guard8 ||
(
guard10 ||
(
guard12 ||
guard14
)
)
)
)
)
)
))
;
guard23 = (
(
guard22_e1 ||
guard22
) &&
guard22
)
;
}
_GO = 0
}
/* G E N E R A T E D C C O D E */
/*****************************************************************************/
/* KIELER - Kiel Integrated Environment for Layout Eclipse RichClient */
/* */
/* http://www.informatik.uni-kiel.de/rtsys/kieler/ */
/* Copyright 2014 by */
/* + Christian-Albrechts-University of Kiel */
/* + Department of Computer Science */
/* + Real-Time and Embedded Systems Group */
/* */
/* This code is provided under the terms of the Eclipse Public License (EPL).*/
/*****************************************************************************/
int second ;;
int contact0 ;;
int contact1 ;;
int track ;;
int _GO ;;
int guard21_e1 ;;
int guard21_e1 ;;
int guard22_e1 ;;
int guard0 ;;
int guard1 ;;
int guard2 ;;
int guard3 ;;
int guard4 ;;
int guard5 ;;
int guard6 ;
int PRE_guard6 ;;
int guard7 ;;
int guard8 ;
int PRE_guard8 ;;
int guard9 ;;
int guard10 ;
int PRE_guard10 ;;
int guard11 ;;
int guard12 ;
int PRE_guard12 ;;
int guard13 ;;
int guard14 ;
int PRE_guard14 ;;
int guard15 ;;
int guard16 ;;
int guard17 ;
int PRE_guard17 ;;
int guard18 ;;
int guard19 ;
int PRE_guard19 ;;
int guard20 ;;
int guard21 ;;
int guard22 ;;
int guard23 ;
int reset(){
_GO = 1;
}
int tick(){
guard0 = _GO;
Tick: {
if (guard1) {
track = 60;
}
guard2 = guard1;
guard15 = (PRE_guard14)
;
guard16 = (
guard15 &&
second
)
;
if (guard16) {
track = 60;
}
guard3 = (
guard2 ||
guard16
)
;
guard20 = (PRE_guard19)
;
guard4 = (
(
guard3 &&
contact0
) ||
(
guard20 &&
contact0
)
)
;
if (guard4) {
track = 20;
}
guard18 = (PRE_guard17)
;
guard5 = (
(
guard4 &&
contact1
) ||
(
guard18 &&
contact1
)
)
;
if (guard5) {
track = 0;
}
guard7 = (PRE_guard6)
;
guard6 = (
guard5 ||
(
guard7 &&
(!(second))
)
)
;
guard9 = (PRE_guard8)
;
guard8 = (
(
guard7 &&
second
) ||
(
guard9 &&
(!(second))
)
)
;
guard11 = (PRE_guard10)
;
guard10 = (
(
guard9 &&
second
) ||
(
guard11 &&
(!(second))
)
)
;
guard13 = (PRE_guard12)
;
guard12 = (
(
guard11 &&
second
) ||
(
guard13 &&
(!(second))
)
)
;
guard14 = (
(
guard13 &&
second
) ||
(
guard15 &&
(!(second))
)
)
;
guard17 = (
(
guard4 &&
(!(contact1))
) ||
(
guard18 &&
(!(contact1))
)
)
;
guard19 = (
(
guard3 &&
(!(contact0))
) ||
(
guard20 &&
(!(contact0))
)
)
;
guard21 = 0;
guard21_e1 = (!((
guard19 ||
(
guard17 ||
(
guard6 ||
(
guard8 ||
(
guard10 ||
(
guard12 ||
guard14
)
)
)
)
)
)
))
;
guard22 = (
(
guard21_e1 ||
guard21
) &&
guard21
)
;
guard22_e1 = (!((
guard19 ||
(
guard17 ||
(
guard6 ||
(
guard8 ||
(
guard10 ||
(
guard12 ||
guard14
)
)
)
)
)
)
))
;
guard23 = (
(
guard22_e1 ||
guard22
) &&
guard22
)
;
}
_GO = 0
}
T2A6