Commit 0338d89d authored by Thanassis Tsiodras's avatar Thanassis Tsiodras

Synced with master branch in GitHub/OpenAADL/ocarina

parents 52d4f524 4f68fc54
# Contributing to Ocarina
## Bugs reports
Ocarina relies on GitHub issues for processing bug reports,
a template is provided that details required information.
## Pull requests
Ocarina welcomes pull requests. Simply follow GitHub pull request mechanism.
Feel free to discuss it first, for instance through a GitHub issue.
Note that all pull requests would have to carefully follow Ocarina coding guidelines and pass all tests.
Note these are done automatically as part of the pull request validation.
......@@ -12,6 +12,7 @@ aclocal.m4
doc/ocarina.info
doc/stamp-vti
doc/version.texi
resources/runtime/aadlib
resources/runtime/polyorb-hi-ada
resources/runtime/polyorb-hi-c
resources/runtime/python/ocarina.pyc
......
......@@ -13,6 +13,7 @@
# GNAT GPL release to compile and run everything.
language: generic
osx_image: xcode8.3
# Global variables
env:
......
......@@ -22,7 +22,9 @@ As a back-end, it supports
* Model checking, using Petri Net `Tina <http://projects.laas.fr/tina//>`_, and `LNT <http://cadp.inria.fr>`_
* Constraint analysis, using the REAL annex language
It can be integrated with the `AADLib <https://github.com/OpenAADL/AADLib>`_ library of AADL components, and through a `OSATE2 plugin <https://github.com/OpenAADL/osate2-ocarina>`_
It can be integrated with the `AADLib <https://github.com/OpenAADL/AADLib>`_ library of AADL components.
It can also be embedded in AADL editors: in `OSATE <http://osate.org>`_ using the `OSATE2 plugin <https://github.com/OpenAADL/osate2-ocarina>`_, and `AADL Inspector <http://www.ellidiss.fr/public/wiki/wiki/inspector>`_
Installation:
-------------
......@@ -36,6 +38,8 @@ Build status for Linux and OS X: |build-status|
Code coverage: |coverage|
CII Best practice: |cii|
.. |build-status| image:: https://travis-ci.org/OpenAADL/ocarina.svg?branch=master
:target: https://travis-ci.org/OpenAADL/ocarina
......@@ -51,3 +55,7 @@ Code coverage: |coverage|
.. |release| image:: https://img.shields.io/github/release/OpenAADL/ocarina.svg
:target: https://github.com/OpenAADL/ocarina/releases
:alt: GitHub Releases
.. |cii| image:: https://bestpractices.coreinfrastructure.org/projects/1019/badge
:target: https://bestpractices.coreinfrastructure.org/projects/1019
:alt: CII Best practice
AC_PREREQ(2.57)
AC_INIT(ocarina, 2017.1)
AC_INIT(ocarina, 2017.x)
AC_CONFIG_SRCDIR(src)
AC_CONFIG_AUX_DIR(support)
......@@ -421,6 +421,7 @@ AC_OUTPUT([
resources/runtime/aadl_xml/Makefile
resources/runtime/alloy/Makefile
resources/runtime/cheddar/Makefile
resources/runtime/lnt/Makefile
resources/runtime/python/Makefile
projects/ocarina.gpr
src/main/Makefile
......
......@@ -6,7 +6,7 @@
-- --
-- P r o j e c t --
-- --
-- Copyright (C) 2007-2009 Telecom ParisTech, 2010-2015 ESA & ISAE. --
-- Copyright (C) 2007-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -36,7 +36,34 @@ project Ocarina.Backends is
Src_Dir := Ocarina.Top_Src_Dir & "/backends";
Build_Dir := Ocarina.Top_Build_Dir & "/backends";
for Source_Dirs use (Src_Dir, Build_Dir);
for Source_Dirs use (Src_Dir, Build_Dir,
Src_Dir & "/aadl_pp",
Src_Dir & "/aadl_xml",
Src_Dir & "/alloy",
Src_Dir & "/arinc653",
Src_Dir & "/arinc653_conf",
Src_Dir & "/asn1_deployment",
Src_Dir & "/ast_ada",
Src_Dir & "/ast_asn1",
Src_Dir & "/ast_c",
Src_Dir & "/ast_xml",
Src_Dir & "/bound-t",
Src_Dir & "/cheddar",
Src_Dir & "/connection_matrix",
Src_Dir & "/deos_conf",
Src_Dir & "/functions_matrix",
Src_Dir & "/lnt",
Src_Dir & "/mast",
Src_Dir & "/petri_nets",
Src_Dir & "/po_hi_ada",
Src_Dir & "/po_hi_c",
Src_Dir & "/real",
Src_Dir & "/stats",
Src_Dir & "/subprograms",
Src_Dir & "/vxwork653_conf",
Src_Dir & "/xtratum_conf"
);
for Object_Dir use Build_Dir & "/objects";
for Library_Dir use Build_Dir & "/libs";
for Library_Name use "ocarina-backends";
......
......@@ -10,7 +10,7 @@ end arm;
processor cortex_m extends arm
properties
Deployment::Execution_Platform => ARM_CORTEX;
Deployment::Execution_Platform => GNAT_Runtime;
end cortex_m;
processor implementation cortex_m.i
......
......@@ -22,6 +22,7 @@ property set Deployment is
(Native, -- Native platforms (GNU/Linux, Solaris, Windows...)
Native_Compcert, -- Native platforms using the Compcert compiler
bench, -- Benchmark platform (native with instrumentation).
GNAT_Runtime, -- Use a GNAT Runtime, e.g. from the Ada_Drivers_Library
LEON_RTEMS, -- LEON2 board or tsim-leon (RTEMS)
LEON_RTEMS_POSIX, -- LEON2 board or tsim-leon (RTEMS)
LEON3_SCOC3, -- LEON3 with RTEMS for SCOC3
......@@ -53,6 +54,15 @@ property set Deployment is
applies to (all);
-- Execution platform of a processor
Ada_Runtime : aadlstring applies to (processor);
-- If Execution_Platform is set to GNAT_Runtime, this property
-- points to the name of the GNAT Project file that configures the
-- Ada_Runtime, e.g. from the Ada Device Drivers project.
USER_CFLAGS : aadlstring applies to (processor);
USER_LDFLAGS : aadlstring applies to (processor);
-- User defined CFLAGS and LDFLAGS
Supported_Execution_Platform : list of Deployment::Allowed_Execution_Platform
applies to (device);
-- List execution platforms supported by a particular driver
......
SUBDIRS = cheddar aadl_xml python alloy
SUBDIRS = cheddar aadl_xml python alloy lnt
@DEBUG_FALSE@DEBUG_FLAG = --disable-debug
@DEBUG_TRUE@DEBUG_FLAG = --enable-debug
......
module LNT_Generic_Process_For_Port_Connections (Types) is
-- No Behavior Annex
-- data port --
process Data_Port [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port]
is
var Data : LNT_Type_Data in
Data := EMPTY;
loop
select
Input (?Data)
[]
Output (Data)
end select
end loop
end var
end process
-- event port --
-- for no periodic threads --
process Event_Port [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
Data : LNT_Type_Data,
FIFO : LNT_Type_Data_FIFO,
Is_New : bool
in
FIFO := {};
Data := EMPTY;
Is_New := false;
loop
select
Input (?Data);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (Data, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO));
FIFO := tail (FIFO)
else
Output (EMPTY)
end if
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
end select
end loop
end var
end process
-- for periodic threads
process Event_Port_For_Periodic [
Input: LNT_Channel_Port,
Output: LNT_Channel_Port](
Queue_Size: Nat)
is
var
Data : LNT_Type_Data,
FIFO : LNT_Type_Data_FIFO,
Is_New : bool
in
FIFO := {};
Data := EMPTY;
Is_New := false;
loop
select
Input (?Data);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (Data, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO));
FIFO := tail (FIFO)
else
Output (EMPTY)
end if
end select
end loop
end var
end process
end module
module LNT_Generic_Process_For_Port_Connections_BA (BA_Types) is -- With Behavior Annex
-- data port --
process Data_Port [
Input: LNT_Channel_Data_Port,
Output: LNT_Channel_Data_Port]
is
var Data : LNT_Type_Data in
Data := DATA_INIT;
loop
select
Input (?Data)
[]
Output (Data)
end select
end loop
end var
end process
-- event port --
-- for no periodic threads --
process Event_Port [
Input: LNT_Channel_Event_Port,
Output: LNT_Channel_Event_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
Nb_Events : Nat,
Is_New : bool
in
Nb_Events := 0;
Is_New := false;
loop
select
Input (true);
Is_New := true;
if (Nb_Events < Queue_Size) then
Nb_Events := Nb_Events + 1
end if
[]
if (Nb_Events > 0) then
Output (true);
Nb_Events := Nb_Events - 1
else
Output (false)
end if
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
end select
end loop
end var
end process
-- for periodic threads --
process Event_Port_For_Periodic [
Input: LNT_Channel_Event_Port,
Output: LNT_Channel_Event_Port](
Queue_Size: Nat)
is
var
Nb_Events : Nat
in
Nb_Events := 0;
loop
select
Input (true);
if (Nb_Events < Queue_Size) then
Nb_Events := Nb_Events + 1
end if
[]
if (Nb_Events > 0) then
Output (true);
Nb_Events := Nb_Events - 1
else
Output (false)
end if
end select
end loop
end var
end process
-- event data port
-- for no periodic threads --
process Event_Data_Port_Sporadic [
Input: LNT_Channel_Event_Data_Port,
Output: LNT_Channel_Event_Data_Port,
Notify: LNT_Channel_Event](
Queue_Size: Nat)
is
var
FIFO : LNT_Type_Data_FIFO,
Is_New : bool,
D : LNT_Type_Data
in
FIFO := {};
D := DATA_INIT;
Is_New := false;
loop
select
Input (?D, true);
Is_New := true;
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (D, FIFO)
[]
if (Is_New) then
Notify (Incoming_Event);
Is_New := false
else
Notify (No_Event)
end if
[]
if (FIFO != {}) then
Output (Head (FIFO), true);
FIFO := tail (FIFO)
else
Output (D,false)
end if
end select
end loop
end var
end process
-- for periodic threads --
process Event_Data_Port_For_Periodic [
Input: LNT_Channel_Event_Data_Port,
Output: LNT_Channel_Event_Data_Port](
Queue_Size: Nat)
is
var
FIFO : LNT_Type_Data_FIFO,
D : LNT_Type_Data
in
FIFO := {};
D := DATA_INIT;
loop
select
Input (?D, true);
if length (FIFO) >= Queue_Size then
FIFO := tail (FIFO)
end if;
FIFO := append (D, FIFO)
[]
if (FIFO != {}) then
Output (Head (FIFO), true);
FIFO := tail (FIFO)
else
Output (D,false)
end if
end select
end loop
end var
end process
end module
AUTOMAKE_OPTIONS = no-dependencies
LNT_FILES = $(srcdir)/LNT_Generic_Process_For_Port_Connections.lnt \
$(srcdir)/LNT_Generic_Process_For_Port_Connections_BA.lnt
EXTRA_DIST = $(LNT_FILES)
lnt_generic = ${shell $(CYGPATH_U) '$(includedir)/ocarina/runtime/lnt'}
install-data-local:
$(INSTALL) -d $(DESTDIR)$(lnt_generic)
for f in $(LNT_FILES); do $(INSTALL) -m 444 $$f $(DESTDIR)$(lnt_generic) ; done