Dezyne Reference Manual

Table of Contents

Next:   [Contents][Index]

Dezyne

This document describes Dezyne version 2.17.2.

• Introduction  What is Dezyne about?
• Ideas and Concepts  Explaining the underlying thinking.
• Installation  Installing Dezyne.
• Getting Started  Writing a program in Dezyne.
• Execution Semantics  How do they do it?
• Formal Verification  A guide to verification errors.
• Defensive Design  A protective armor.
• Code Integration  Creating an executable.
• The Dezyne command-line tools  Running the tools.
• Dezyne Language Reference  All the language details.
• Well-formedness  Interpreting parse errors.
• Contributing  Your help needed!
• Concept Index  Concepts.
• GNU Free Documentation License  The license of this manual. 


 — The Detailed Node Listing —

Introduction
• Purpose  Why are we creating Dezyne?
• Conditions for Using Dezyne  There are (almost) no limits to using Dezyne. 

Ideas and Concepts
• Concurrency  A message passing programming model.
• Component Based  Recursive decompositioning.
• Model Based  Modeling the real world.
• Design by Contract  Contracts for message interaction.
• Managing Complexity  Abstraction and encapsulation. 

Installation
• Requirements  Software needed to build and run Dezyne. 

Getting Started
• Hello World!  First contact with Dezyne.
• A Simple State Machine  Stateful behavior and protocol.
• A Camera Example  A System of Components and Systems.
• The Lego Ball Sorter  A Machine Operating System. 

Execution Semantics
• Direct in event  A provides trigger forwarded
• Direct out event  A requires trigger forwarded.
• Direct multiple out events  Multiple requires triggers forwarded.
• Indirect in event  A requires trigger => requires action.
• Indirect out event  A provides trigger => provides trigger via requires action.
• Indirect multiple out events  Provides trigger => provides trigger via requires actions and triggers.
• Indirect blocking out event  Synchronize two triggers via block and release.
• External multiple out events  Delay caused by parallelism
• Indirect blocking multiple external out events  Block, delay, release.
• Multiple provides  Multiple provides ports
• Blocking multiple provides  Blocking and multiple provides ports
• Blocking in system context  Blocking by one level of indirection: collateral blocking 

Formal Verification
• Verification Checks and Errors  Which properties are verified?
• Verification Counter Examples  What if verification fails?
• Interpreting Verification Errors  How to fix verification errors. 

Defensive Design
• Interface Contracts  Consequences of a breach of contract.
• Error Handling and Recovery  Specifying Exceptional behavior.
• Armoring  Making a program robust. 

Code Integration
• Integrating C++ Code  
• Foreign Component  
• Thread-safe Shell  
• Integrating Scheme Code   

Integrating Scheme Code
• Namespace to Module   

The Dezyne command-line tools
• Invoking dzn  Running Dezyne commands.
• Invoking dzn code  Generating code from a Dezyne file.
• Invoking dzn graph  Generating graphs of Dezyne models.
• Invoking dzn hello  A simple sanity check.
• Invoking dzn language  Lookup and completion.
• Invoking dzn lts  Manipulate and query an LTS.
• Invoking dzn parse  Checking the syntax of Dezyne file.
• Invoking dzn simulate  Simulating Dezyne models.
• Invoking dzn trace  Transform verify, code, and simulate traces.
• Invoking dzn traces  Generate a set of traces.
• Invoking dzn verify  Verifying Dezyne models. 


Dezyne Language Reference
• Lexical Analysis  Tokens, separators and whitespace.
• Dezyne Files  What goes into a Dezyne file?
• Types and Expressions  Manipulating data in Dezyne.
• Interfaces  Defining contracts for components and systems.
• Components  Defining a program’s behavior in Dezyne.
• Systems  Decomposing a system.
• Namespaces  Avoiding name collision. 

Lexical Analysis
• Identifiers  Choosing names.
• Keywords  Restricted words.
• Operators  Building blocks for expressions.
• Delimiters  Constructing lists.
• Lexical Scoping  Locality of names.
• Comments  Explanations for human readers. 

Types and Expressions
• Void  Definitions without type.
• Bool  Builtin boolean type.
• Enum  Enumerated user types.
• Subint  Integer user types.
• Extern Data Type  Foreign data user types.
• Expressions  Constants and data. 

Interfaces
• Events  Event or message definitions.
• Behavior  Specifying an interface protocol.
• Declarative Statements  Define when to run which trigger.
• Imperative Statements  The code that runs upon a trigger.
• Functions  Avoiding code duplication. 

Behavior
• Behavior Variable  The detailed state of the behavior. 

Declarative Statements
• On  Defining what happens upon a trigger.
• Guard  Declarative trigger condition.
• Using inevitable and optional  Nitty gritty details on using modeling events. 

Imperative Statements
• Action  Emitting events.
• Assign  Updating state.
• Function Call  A named collection of imperative statements.
• Empty Statement  When a trigger has no effect, or there is nothing to do.
• If  Imperative decisions.
• Illegal  Specifying what is not allowed.
• Reply  Determining the reply for a valued trigger.
• Return  Returning from a function.
• Variable  Defining a local variable. 

Components
• Ports  Defining a component’s communication channels.
• Component Behavior  Defining a component’s behavior.
• Component Types  Three types of components.
• Component Declarative Statements  Component-specific declarative statements.
• Component Imperative Statements  Component-specific imperative statements.
• Multiple Provides Ports  Providing more than one interface. 

Ports
• Injection  Ports sharing a resource.
• External  Ports with external delay. 

Component Declarative Statements
• Component On  Defining what happens on a trigger.
• Blocking  Implementing a synchronous call on decoupled events.
• Formal Binding  Parameter assignment in blocking or synchronous out context.
• Joining Activities  A full blocking example. 

Component Imperative Statements
• Component Action  Sending messages over ports.
• Component If  Imperative decisions in a component.
• Component Illegal  Using illegal in a component.
• Component Reply  Using reply in a component.
• Component Defer  Decoupling execution from the client. 

Systems
• Component Instances  The components of a system.
• Binding  The plumbing of a system. 

Binding
• Using Injection  Binding injected ports. 

Well-formedness
• Well-formedness Checks Categories  Types of checks.
• List of Well-formedness Checks  An alphabetical lookup list.
• Well-formedness -- Top level  Interfaces, events and components.
• Well-formedness -- Directional  Direction of trigger and action.
• Well-formedness -- Nesting  The right place for declarative and imperative.
• Well-formedness -- Mixing  Mixing of declarative and imperative.
• Well-formedness -- Reply  Reply and ports.
• Well-formedness -- Valued Actions and Calls  Careful use of values.
• Well-formedness -- Injection  Restrictions on injection.
• Well-formedness -- Functions  Returning and recursing.
• Well-formedness -- Data Parameters  Data type errors.
• Well-formedness -- System  Correctly binding all ports. 

Well-formedness – Top level
• Interface must define an event  
• Interface must define a behavior  
• Out-event must be void  
• Component with behavior must have a trigger  
• Component with behavior must define a provides port   

Well-formedness – Directional
• Cannot use event as action  
• Cannot use event as trigger   

Well-formedness – Nesting
• Assign outside on  
• Action outside on  
• Nested on used  
• Nested blocking used  
• Cannot use blocking in an interface   

Well-formedness – Mixing
• Declarative statement expected  
• Imperative statement expected  
• Cannot use otherwise guard more than once  
• Cannot use otherwise guard with non-guard statements  
• Cannot use illegal with imperative statements  
• Cannot use illegal in if-statement  
• Cannot use illegal in function   

Well-formedness – Reply
• Must specify provides-port with reply on out-trigger  
• Must specify provides-port with reply   

Well-formedness – Valued Actions and Calls
• Action in member variable initializer  
• Call in member variable initializer  
• Action value discarded  
• Call value discarded   

Well-formedness – Injection
• Injected port has out-events   

Well-formedness – Functions
• Missing return  
• Cannot use return outside of function  
• Cannot use statement after recursive call   

Well-formedness – Data Parameters
• Type mismatch -- parameter expected extern  
• Cannot use out-parameter on out-event  
• Cannot use inout-parameter on out-event  
• Formal binding is not a data member variable   

Well-formedness – System
• Port not bound  
• Port not bound -- of instance  
• Port is bound more than once  
• Cannot bind port to port  
• Cannot bind two wildcards  
• Instance is in a cyclic binding  
• Cannot bind wildcard to requires port  
• System composition is recursive  
• Cannot bind external port to non-external port   

Contributing
• Building from Git  The latest and greatest.
• Running Dezyne Before It Is Installed  Hacker tricks.
• The Perfect Setup  The right tools.
• Coding Style  Hygiene of the contributor.
• Submitting Patches  Share your work. 

Coding Style
• Programming Paradigm  How to compose your elements.
• Data Types and Pattern Matching  Implementing data structures.
• Formatting Code  Writing conventions.

Next:   [Contents][Index]