CIF 3

Index

Symbols | A | B | C | D | E | F | G | H | I | J | L | M | N | O | P | R | S | T | U | V | W | Y

Symbols

!
channel parameter usage restriction
4K420
#, [1]
actuators
course files
emergency button
event names
exercise 1
exercise 2
exercise 3
exercise 4
exercises
flow shop system
getting started
initialization
initialization problems
input station
installation
naming convention, [1]
performance
process station
scripts
sensors
storage station
supervisory control
terminology
test station
timers
toolchain
tooling
user interface
workstations
?
channel parameter usage restriction
~
channel parameter usage restriction

A

add default initial values
implementation
optimality
preprocessing
renaming
size considerations
supported specifications
addressable
algebraic variable
eliminate
equation
alphabet, [1]
default
explicit
global event disablement
implicit
implicit vs explicit
minimum
non-default
array
see also list
assignment
addressable
left hand side
multi-assignment
multiple
order
right hand side
value
automata to string casts
eliminate
automatic input mode
automatic mode choice algorithm option
automatic mode transition duration option
limitations
automaton, [1]
alphabet, [1]
definition
instantiation
kindless
monitor
plant, [1]
regular
requirement, [1]
supervisor, [1]
supervisory kind
automaton definition
parameters, [1]
automaton definition parameter
algebraic
automaton
channel
component
event
location
multiple
see also channel parameter usage restriction
automaton instantiation
arguments, [1]
automaton self reference
eliminate

B

backward incompatible language changes
boolean
literal
type
value

C

C4C
C99
code generation
channel
dataless
declaration
receive
received value
receiver
send
sender
synchronization
void
channel parameter usage restriction
!
?
flags
~
CIF 3 code generator
C99
Java
Simulink
options
preprocessing
start
supported specifications
CIF 3 event disabler
options
output
performance
preprocessing
specifying events
start
supported specifications
usage scenario
CIF 3 merger
example
invariants
merge compatibility
merge problems
options
preprocessing
shared events
shared variables
start
CIF 3 PLC code generator
I/O coupling
IEC 61131-3
PLCopen XML
TwinCAT
accuracy over time
generated code
names
options
output types
preprocessing
program body
see TwinCAT
standard compliance
start
supported specifications
CIF 3 simulator
Java compiler
ODE solver
SVG visualization
complete mode
console output
deadlock
debug generated code
debug output
environment events
external user-defined functions
fixed output step size
history
initialization
input components
input modes
maximum delay
maximum time point tolerance
non-urgent events
normal output
options
output
output components
performance
plot visualizer
print output
profiling
real-time simulation
repeated simulation
reset
runtime error
simulation end time
simulation of traces
start
starting with generated code
state visualizer
stochastic distributions
supported specifications
termination
test mode
trajectory data
undo
CIF explorer
options
preprocessing
start
supported specifications
CIF to CIF transformer
add default initial values
available transformations
convert switch expressions to if expressions
eliminate algebraic variables
eliminate automata to string casts
eliminate automaton self references
eliminate component definition/instantiation
eliminate constants
eliminate enumerations
eliminate equations
eliminate groups
eliminate if updates
eliminate monitors
eliminate state/event exclusion invariants
eliminate tau event
eliminate the use of locations in expressions
eliminate tuple field projections
eliminate type declarations
lift events
linearize (merge)
linearize (product)
merge enumerations
options
pretty printer
push SVG file declarations into other CIF/SVG declarations
push print file declarations into print declarations
rationale
remove CIF/SVG declarations
remove I/O declarations
remove position information
remove print declarations
remove requirements
simplify others
simplify values
simplify values (no references)
simplify values (no references, optimized)
simplify values (optimized)
start
transformation descriptions
CIF to mCRL2 transformer
debug output
generation of value actions
instance tree
options
preprocessing
result of the transformation
start
supported specifications
CIF to Supremica transformer
alphabets
initialization
invariants
jumping semantics
marking
options
preprocessing
range semantics
start
supported specifications
transformation result
CIF to UPPAAL transformer
options
preprocessing
start
supported specifications
transformation result
CIF to yEd transformer
diagram kinds
layout
options
preprocessing
start
supported specifications
CIF/SVG declaration
remove
see also SVG declaration
component, [1], [2]
automaton
automaton instantiation
definition
group
group instantiation
component definition
eliminate
component instantiation
eliminate
CON4COORD
see C4C
constant
eliminate
expression
value
contact
continuous variable
derivative
equation
controllable event
convert switch expressions to if expressions
implementation
optimality
size considerations
course files
4K420

D

data-based
synthesis
data-based supervisory controller synthesis
checks
debugging
forward reachability
initialization
input variables
operation caches
options
performance
preprocessing
requirements
resulting supervisor
simplification
start
statistics
supported specifications
variable order
data-based synthesis
deadlock
debug
PLC code
SVG input
SVG visualization
generated code
maximum delay
print output
simulator debug console output
debug console output
option
declaration
multiple
order
derivative
continuous variable
equation
dictionary
literal
pair
type
value
discrete event system
discrete variable
initial value
value change
do
download

E

edge, [1]
assignment
do
guard, [1]
labeling
multiple events
no events
self loop, [1], [2]
take
update, [1]
when
eliminate algebraic variables
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate automata to string casts
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate automaton self references
implementation
preprocessing
size considerations
supported specifications
eliminate component definition/instantiation
implementation
size considerations
eliminate constants
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate enumerations
implementation
preprocessing
renaming
size considerations
supported specifications
eliminate equations
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate groups
implementation
preprocessing
renaming
size considerations
supported specifications
eliminate if updates
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate monitors
implementation
optimality
preprocessing
size considerations
supported specifications
eliminate state/event exclusion invariants
implementation
optimality
preprocessing
renaming
size considerations
supported specifications
eliminate tau event
implementation
renaming
size considerations
eliminate the use of locations in expressions
implementation
optimality
preprocessing
renaming
size considerations
supported specifications
eliminate tuple field projections
implementation
size considerations
eliminate type declarations
implementation
preprocessing
size considerations
supported transformations
enabledness
event
enumeration
declaration
eliminate
literal
merge
type
value
environment events
input modes
supervisory control application domain
equation
algebraic variable
benefit
continuous variable
derivative
eliminate
event, [1]
channel
controllability
controllable, [1]
declaration, [1]
disabled
enabled
enabledness, [1]
input
interactive
lift to specification
multiple on edge
placement
state/event exclusion invariant;
synchronize
tau
uncontrollable, [1]
urgency, [1]
event-based
synthesis
event-based automaton abstraction
event-based synthesis toolset
options
start
event-based automaton projection
event-based synthesis toolset
options
start
event-based controllability check
event-based synthesis toolset
options
start
supported specifications
event-based DFA minimization
event-based synthesis toolset
start
event-based language equivalence check
event-based synthesis toolset
options, [1]
start
event-based NFA to DFA automaton conversion
event-based synthesis toolset
options
start
event-based nonconflicting check
event-based synthesis toolset
options
start
event-based observer check
event-based synthesis toolset
options
start
event-based supervisor synthesis
event-based synthesis toolset
options
start
supported specifications
event-based supervisory control
see event-based synthesis toolset
event-based synchronous product
event-based synthesis toolset
options
start
event-based synthesis
event-based synthesis analysis
event-based synthesis analysis toolset
start
event-based synthesis analysis toolset
event-based synthesis analysis
event-based synthesis toolset
automaton kinds
event-based DFA minimization
event-based NFA to DFA automaton conversion
event-based automaton abstraction
event-based automaton projection
event-based controllability check
event-based language equivalence check
event-based nonconflicting check
event-based observer check
event-based supervisor synthesis
event-based synchronous product
event-based trim
event-based trim check
names in errors
names in reports
preprocessing
supported specifications
tools
event-based trim
event-based synthesis toolset
options
start
event-based trim check
event-based synthesis toolset
options
start
examples
execution
explorer
see CIF explorer
expression
computation
constant
evaluation
literal
external user-defined functions
Java
asynchronous execution
call by value
determinism
logging
responsiveness
side effects
synchronous execution
termination
value semantics
external user-defined Java functions
Java Virtual Machine, [1]
class loader, [1]
implementation reference
lazy loading
method invocation
method modifier
method resolution
runtime errors
side effects
state
static data
static method
stderr
stdout
supported types
supported values

F

fixed point
flags
channel parameter usage restriction
format specifier
%B
%E
%G
%S
%X
%b
%d
%e
%f
%g
%s
%x
alignment
explicit indexing
flags
grouping
implicit indexing
indexing
justification
leading space
padding
sign
syntax
thousand separator
width
zero padding
formula
modal logic controlled system synthesis
frame
intermediate
function
application
body
call
internal
internal vs external
local variables
parameters
return type
return value
side effects
standard library
statements, [1]
user-defined
function statements
assignment
break
continue
if
return
while

G

goto
group
definition
eliminate
instantiation
namespace
guard, [1]
multiple
splitting

H

hybrid system
HYCON2

I

I/O declaration
SVG copy declaration
SVG declaration
SVG file declaration
SVG input mapping
SVG move declaration
SVG output mapping
print declaration
print file declaration
remove
if update
eliminate
import
directories
group merging
library
initial
initial value
any
default
discrete variable
explicit
implicit
multiple
initialization
consistency, [1]
cyclic dependencies
predicate
restricted
Inkscape
XML editor
changing ids
coordinate system
document size
flowRoot
height
text area
width
input component
see input mode
input mode
SVG input mode
automatic input mode
interactive GUI input mode
interactive console input mode
overview
semi-automatic mode
trace input mode
input variable
co-simulation example
hardware example
merging CIF models
installation
integer
limits
literal
overflow
range
type
value
integrator options
algorithm
number of steps
step sizes
tolerances
interactive console input mode
semi-automatic mode
interactive GUI input mode
semi-automatic mode
invariant, [1], [2]
eliminate state/event exclusion invariants
kindless
plant
regular
requirement, [1]
state
state/event exclusion
supervisor
supervisory kind

J

Java
code generation

L

language
features
history
lift events
implementation
preprocessing
renaming
size considerations
supported specifications
linearize
communication, [1]
implementation, [1]
merge
non-determinism, [1]
optimality, [1]
order, [1]
preprocessing, [1]
product
received values, [1]
renaming, [1]
size considerations, [1]
supported specifications, [1]
tuple field projections, [1]
urgency, [1]
list
bounded
concatenation
indexing
limits
literal
maximum size
projection
regular
slicing
type
value
literal
boolean
dictionary
enumeration
expression
integer
list
real
set
string
tuple
value
livelock
location, [1], [2]
active
as variable
initial, [1]
invariant
marked
nameless
urgency
versus variable, [1]

M

marker
predicate
marking, [1]
mCRL2
see CIF to mCRL2 transformer
merge enumerations
default initial values
implementation
preprocessing
renaming
size considerations
supported specifications
migration
modal logic controlled system synthesis
preprocessing
supported specifications
model, [1]
monitor
eliminate
monitoring
monitor automaton
self loops
Multiform

N

namespace
non-determinism
normal console output
option
output details
state filtering

O

observing
see monitoring
ODE
IVP
bisection
bracketing
discontinuity
fixed output step size
guard splitting
integration
integrator options
interval
linear ODE
maximum check interval
maximum delay
nonlinear ODE
numeric integration
numeric root finding
root finder options
root finding
root finding problem
simulation end time
step size
ODE solver
see ODE
optimized)
implementation
optimality
preprocessing
size considerations
supported specifications
output component
real-time
output components
see simulation output

P

performance
CIF 3 event disabler
Java compiler
SVG input
asynchronous external user-defined functions
compile once
integrator step sizes
position information
repeated simulation
root finding maximum check interval
simulation
simulation frame rate
supervisory control
plant, [1]
automaton
PLC
see CIF 3 PLC code generator
see CIF 3 code generator
plot visualizer
data points
disable
enable
filtering
modes
multiple
range
reset
save plot image
trajectory data relation
undo
pretty printer
see CIF to CIF transformer
print
declaration
print declaration
combining filters
escaping
extended trace
file
post text
pre text
push
quoting
remove
scoping
state filtering
stderr
stdout
target
text to print
transition centric view
transition filtering
virtual labels
print file declaration
path
push
remove
scoping
special target
stderr
stdout
uniqueness
print output
disable
enable
example
examples
footer
header
line-based
order
overwrite
print declaration
print file declaration
printing to file
reset
simulation
text formatting, [1]
tutorial
undo
printfile
see print file declaration
profiling
debug console output
normal console output
see CIF 3 simulator
property
publications
push print file declarations into print declarations
implementation
preprocessing
size considerations
supported specifications
push SVG file declarations into other CIF/SVG declarations
implementation
preprocessing
size considerations
supported specifications

R

reachability
backward
forward
real
literal
type
value
real-time simulation
disable
enable
frame
frame rate
intermediate frame
intermediate state
model time delta
simulation speed
test mode
trajectory data
remove CIF/SVG declarations
implementation
size considerations
remove I/O declarations
implementation
size considerations
remove position information
implementation
size considerations
remove print declarations
implementation
size considerations
remove requirements
reporting
bugs
crashes
requirement, [1]
automaton
invariant
remove
root finder options
Illinois
Pegasus
Regula Falsi
algorithm
false position
maximum check interval
maximum iterations
tolerances

S

scripting
seed
CIF 3 simulator normal console output
automatic mode choice algorithm option
automatic mode transition duration option
stochastic distributions
self loop, [1]
set
difference
intersection
literal
type
union
value
simplify others
preprocessing
size considerations
supported specifications
simplify values
implementation
optimality
preprocessing
size considerations
supported specifications
simplify values (no references, [1], [2], [3], [4]
simplify values (no references)
implementation
optimality
preprocessing
size considerations
supported specifications
simplify values (no references, optimized)
simplify values (optimized)
implementation
optimality
preprocessing
size considerations
supported specifications
simulation, [1]
urgency
simulation output
SVG visualization
console
debug console output
normal console output
plot visualizer
print output
real-time
state visualizer
trajectory data
simulator
compiled code file
Simulink
code generation
single
state space; explorer
state space; generator
source code
specification
configuration
parameterization
state, [1], [2]
intermediate
invariant
state/event exclusion invariant;
state space, [1]
state visualizer
contents
disable
enable
filtering
icons
legend
multiple
reset
undo
updates
stochastics
constant
continuous
discrete
distribution
sampling
string
literal
type
value
supervisor, [1]
automaton
supervisory control
#, [1]
4K420
4K420 exercises
conflicting supervisors
empty supervisor
event disabler phase
getting started
implementation phase
incremental development
marking
modeling plants
modeling requirements
naming convention, [1]
performance
scalability
scripts
see also synthesis
simulation and traces
simulation phase
simulation vs implementation
specification phase
supervisor inspection phase
supervisor synthesis phase
terminology
timers
toolchain
supervisory controller synthesis
support
Supremica
see CIF to Supremica transformer
SVG
Inkscape
W3C
XML
colors
copy declaration
declarations
flowRoot
id
input event
input mapping
input mode
interactive event
interactivity
move declaration
output mapping
see also SVG visualization
text
tspan
tutorial
viewer
visualization
SVG copy declaration
application
example
file
id
order, [1]
overlap
placement
post
postfix
pre
prefix
root
syntax
uniqueness
SVG declaration
SVG copy declaration
SVG input mapping
SVG move declaration
SVG output mapping
push
SVG file declaration
completeness
path
push
scoping
uniqueness
SVG input mapping
completeness
if event input mapping
single event input mapping
uniqueness
SVG input mode
debugging
frame rate
hovering
interactive groups
performance
queue
responsiveness
simulation
SVG move declaration
application
conflicts
coordinates
example
file
graphical elements
id
order
syntax
to
x
x coordinate
y
y coordinate
SVG output mapping
CSS style attributes
SVG presentation attributes
application
attribute
escaping
example
file
id
order
quoting
spaces
syntax
tabs
text
text labels
type
uniqueness
value
whitespace
SVG viewer
GIF
JPEG
PNG
SVG
export
refresh
save as
SVG visualization
Batik
SVG file declaration
SVG standard
application order
buffers/products example
colors
console output
coordinate systems
copy example
copy of a copy
debugging
demo
disable
enable
examples
export
first example
grouping, [1]
lamps example
literal values
move example
rate example
record
reset
runtime error
save as
scalability, [1], [2]
scaling, [1]
see also SVG
simple solutions
simulation
stack trace
sun/moon example
tank example
text formatting
undo
updating multiple attributes
variable width
visibility
visualizer
walk example
workstation example
y-axis invert trick
SVG visualizer
see SVG viewer
see SVG visualization
svgcopy
see SVG copy declaration
svgfile
see SVG file declaration
svgin
see SVG input mapping
svgmove
see SVG move declaration
svgout
see SVG output mapping
switch expression
convert
synchronization, [1]
eliminate, [1]
guards
tau
synthesis
algorithm
data-based, [1]
distributed
event-based
modal logic
modular
monolithic

T

tau
event
explicit
implicit
synchronization
tau event
eliminate
test mode
SVG debugging
real-time simulation
text formatting, [1]
%%
columns
conversions
escaping
format patterns
format specifiers
introduction
large numbers
left alignment
lower case
quoting
real values
reference documentation
tutorial
unused values
upper case
time
variable
timed system, [1]
timing
tools
CIF 3 PLC code generator
CIF 3 code generator
CIF 3 event disabler
CIF 3 merger
CIF 3 simulator
CIF explorer
CIF to CIF transformer
CIF to Supremica transformer
CIF to UPPAAL transformer
CIF to mCRL2 transformer
CIF to yEd transformer
data-based supervisory controller synthesis
event-based DFA minimization
event-based NFA to DFA automaton conversion
event-based automaton abstraction
event-based automaton projection
event-based controllability check
event-based language equivalence check
event-based nonconflicting check
event-based observer check
event-based supervisor synthesis
event-based synchronous product
event-based synthesis analysis
event-based trim
event-based trim check
modal logic controlled system synthesis
overview
pretty printer
scripting
text editor
trace, [1]
trace input mode
trajectory data
ODE solver
disable
enable
file
filtering
fixed output step size
output
prettify
real-time simulation
reset
see ODE
time points
types
undo
transition, [1]
event
time
tuple
eliminate field projections
indexing
literal
packing
projection
type
unpacking
value, [1]
tutorial
SVG
language
print output
text formatting
TwinCAT
DUT
FAQ
GVL
POU
PlcTask
change mode
config mode
generated output
run mode
system modes
usage
type
boolean
declaration
dictionary
enumeration
integer
list
real
set
string
tuple
type declaration
eliminate

U

ulp
uncontrollable event
update, [1]
4K420 course files
examples
language
UPPAAL
see CIF to UPPAAL transformer
urgency
event, [1]
location
simulation
urgent
see also urgency

V

validation
value, [1]
boolean
constant
dictionary
enumeration
integer
list
literal
real
set
string
tuple
variable, [1]
?
algebraic
continuous
different kinds
discrete
input
new value
old value
read
time
versus location, [1]
write
void
channel

W

when

Y

yEd
Structure View
layout
see CIF to yEd transformer