The CORE components

The Core Definition language (CDL)

This is our common intermediate language for describing any specification. In some aspects it can be compared to the Assembly language.

XML

Their is an XML version of the CDL. It is described under the XML section of the VeriTech project

The Core Parser

This is a C library that parse a textual core program and generates a memory data structure that represents the CDL program.

The Stand alone Core Parser

This is a small application that activate the Core Parser. The application do not generate any output (beside the parsing log) and it main goals are:

  1. Run the Core Parser to check the syntax of a CDL program
  2. Use debugger to follow the parsing of a CDL program and to get deep understanding of how the Core Parser works.
  3. This simple program is the first step for any "core to" translation .

Tree

Tree is the data structure used to store the effective representation of core program. It might (and ought) to be used in any Core2A translation where A is the language that either doesn't support module structure or requires significant changes of original core modules.

Each node of the Tree contains the following information:

modulenode_type Type

-

one of five possible types of modules : Transition, Instantiation, Full/Partial Synchronous and Asynchronous

modulenode_type Prev_type

-

type of node before the handling of synchronization

ModuleNode* Left

-

the node on the left

ModuleNode* Right

-

the node on the right

Module* Module

-

actual module associated with the node
(if there are more than one instance if the same module in program, then copies of module appear in appropriate nodes in tree)

PairSet* Sync

-

the set of pairs of names of transitions that  are synchronized (in case of partial or full synchronization)

ActualParameterSet* Params

-

actual parameters of the module instantiation

RenameSet* Renames

-

Rename set that hold the renames for the  transitions in case the node contains module that is of transition type. In case the node is of the other type, contains the renames for the pairs that are synchronized to allow additional synchronization on the upper level.

Following field can be used as auxiliary in translations:

TransitionSet* ChangedTrans

 -

set of transitions that originally were standalone in module and now are synchronized

TransitionSet* SyncTrans

 -

set of transitions that are synchronized in the module

PairSet* ChangedNames

 -

Pair set that holds the name changes following the synchronization handling
Left part of the pair is the synchronization pair that affected the change of name
Right pat of the pair is the new name given to each transition that appears in synchronization.

PairSet* CurrChanges

 -

Pair set that holds the name changes that are made during the handling of the current synchronous node.Used for the full synchronization and consequent pairs partial synchronization when changes are to be applied on the original names of the transitions from before beginning of handling the node.

 

Flat

Flat utility is used to transform any input core program to equivalent one that is flattened version of the input program. A flattened program, is a program that contains only one module  with transitions inside, that is equivalent in its properties to the original program. Flat utility receives CoreProgram* to original program and returnes CoreProgram* to flattened program.

Flattened program properties:

  1. Local variables and defines from all modules are transferred to global level(name collision resolved by adding name of module where local variable was declared)
  2. Program contains single module with transitions that are equivalent to all transitions from original program combined according to modules compositions.

Steps of the Flat utility:

  1. Creates the Tree to store the program
  2. Transfers all local variables and defines from tree node's modules to global level
  3. Replaces formal parameters in all modules in the tree with actual ones that are used for module's instantiation.
  4. Flattens the tree by performing the following steps:
    1. Perform post-order traversal (post-order insures that when node is handled its sons had already been handled and contain only transitions) of the tree
    2. For each node perform operation according to its type as follows:
      1. NODE_TRANS (node contains module that includes only transitions)
        If module contains cojoin then it is applied on transitions enable rules;  transition set is remained the same otherwise.
      2. NODE_INST (node contains module that instantiates another module)
        transitions from instantiated module are copied to the current one.
      3. NODE_COMBI_ASYNC (node contains asynchronous combination of modules)
        transitions from both modules are collected into set of transitions of current node.Name ambiguities are resolved by adding name of the module where the transition was declared.
      4. NODE_COMBI_SYNC (node contains full synchronous combination of modules)
        cartesian product of each transition from left son and right son is added to current node.In case when in carthesian product two assignments give different value to the same variable warning is issued and resulting transition is excluded from the current node. Name changes of transitions are saved in current node in form of set of pairs (old_name,new_name).
      5. NODE_COMBI_PART (node contains partial synchronization of modules)
        For each synchronization pair collect transitions from left and right sons that are to be synchronized accoring to the pair.Add carthesian product of those transitions
        (each transition from left son combined with each transition from right son) to the transition set of the node.Add all transitions from left and right sons that are not synchronized to the transition set of the current node.
    3. Rename transitions in resulting node according to renaming set in original program.

XML converter

This library converts core data structure to an xml data structure

Core to XML

A small application that converts a textual CDL program to an XML core program.