diff --git a/configure.ac b/configure.ac index 606b77f96ad0e5f48b52bc6a5a2c21408e9ea991..466e4f4edd71aff225c64ed0f126f3641f63ae31 100644 --- a/configure.ac +++ b/configure.ac @@ -97,7 +97,7 @@ AC_OUTPUT([ examples/isr/Makefile examples/line_follower/Makefile examples/memory/Makefile - examples/minepump/Makefile + examples/minepump/Makefile examples/mixin/Makefile examples/mjpeg/Makefile examples/mosart/Makefile @@ -106,6 +106,7 @@ AC_OUTPUT([ examples/pathfinder_system/Makefile examples/perseus/Makefile examples/producer_consumer/Makefile + examples/producer_consumer_ba/Makefile examples/radar/Makefile examples/rap/Makefile examples/rap_code/Makefile diff --git a/examples/Makefile.am b/examples/Makefile.am index d10da60b244280e68f6dfdc3d92e1cb861bda816..14b848cf7ad1e79308df1f4c138e66a5b5373450 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -4,7 +4,8 @@ SUBDIRS= adiru ahrs_discovery aocs aram ardupilot arinc653_annex asl \ pathfinder_system perseus producer_consumer ravenscar radar \ rap rap_code redundancy rma robot round_robin time_triggered \ units uxv voter satellite stm32discovery_ada robot_ba \ - pacemaker doors rosace mjpeg crazyflie air minepump + pacemaker doors rosace mjpeg crazyflie air minepump \ + producer_consumer_ba EXTRA_DIST=$(srcdir)/Makefile.common diff --git a/examples/producer_consumer_ba/Makefile.am b/examples/producer_consumer_ba/Makefile.am new file mode 100644 index 0000000000000000000000000000000000000000..52f7795d6b9204bf40ea6d21296717471b113fac --- /dev/null +++ b/examples/producer_consumer_ba/Makefile.am @@ -0,0 +1,12 @@ +AADL_SOURCES = $(srcdir)/producer_consumer_ba.aadl +AADL_ROOT = pc_simple.native + +OTHER_FILES = + +CLEANDIRS = pc_simple_native +CLEANFILES = *.lnt demo.svl + +include $(srcdir)/../Makefile.common + +AVAILABLE_TARGETS= parse-aadl build_c + diff --git a/examples/producer_consumer_ba/devicesconf.c b/examples/producer_consumer_ba/devicesconf.c new file mode 100644 index 0000000000000000000000000000000000000000..5e3a0b2555a8374e4b42d06e67efedfd9e0a04d5 --- /dev/null +++ b/examples/producer_consumer_ba/devicesconf.c @@ -0,0 +1,4 @@ +#include + +__po_hi_c_ip_conf_t pohidrv_device_a = { .devname = "eth0", .address = "127.0.0.1", .version = __po_hi_c_ipv4, .port = 1234}; +__po_hi_c_ip_conf_t pohidrv_device_b = { .devname = "eth0", .address = "127.0.0.1", .version = __po_hi_c_ipv4, .port = 1235}; diff --git a/examples/producer_consumer_ba/producer_consumer.c b/examples/producer_consumer_ba/producer_consumer.c new file mode 100644 index 0000000000000000000000000000000000000000..647e9fffc2468c47e9aae5f23adfc836e6c0aeba --- /dev/null +++ b/examples/producer_consumer_ba/producer_consumer.c @@ -0,0 +1,8 @@ +#include +#include + +void print_spg +(producer__consumer__alpha_type a_data_in) { + + printf("%d\n", a_data_in); +} diff --git a/examples/producer_consumer_ba/producer_consumer_ba.aadl b/examples/producer_consumer_ba/producer_consumer_ba.aadl new file mode 100644 index 0000000000000000000000000000000000000000..82365b6f7771de8684388f6826c09ba2efa34ed8 --- /dev/null +++ b/examples/producer_consumer_ba/producer_consumer_ba.aadl @@ -0,0 +1,177 @@ +package Producer::Consumer +public + with Deployment; + with Data_Model; + with Buses::Ethernet; + with Processors; + with Native_Sockets; + + ---------- + -- Data -- + ---------- + + data Alpha_Type + properties + Data_Model::Data_Representation => Integer; + end Alpha_Type; + + ----------------- + -- Subprograms -- + ----------------- + + subprogram Produce_Spg + features + Data_Source : out parameter Alpha_Type; + end Produce_Spg; + + subprogram implementation Produce_Spg.Impl + annex behavior_specification {** + states + s : initial final state; + transitions + s -[ ]-> s { Data_Source := 1; + Print_Spg!(Data_Source) }; + **}; + end Produce_Spg.Impl; + + subprogram Print_Spg + features + A_Data_In : in parameter Alpha_Type; + properties + Source_Language => (C); + Source_Name => "print_spg"; + Source_Text => ("producer_consumer.c"); + end Print_Spg; + + subprogram Consume_Spg + features + Data_Sink : in parameter Alpha_Type; + properties + Source_Language => (C); + Source_Name => "consume_spg"; + Source_Text => ("producer_consumer.c"); + end Consume_Spg; + + ------------- + -- Threads -- + ------------- + + thread P + features + Data_Source : out event data port Alpha_Type; + -- XXX Data seems corrupted if Data_Source is an out data port + properties + Dispatch_Protocol => Periodic; + Compute_Execution_Time => 1 ms .. 10 ms; + Priority => 1; + Period => 500 ms; + end P; + + thread implementation P.Impl + calls + Mycall : { + P_Spg : subprogram Produce_Spg.Impl; + }; + connections + Z1:parameter P_Spg.Data_Source -> Data_Source; + end P.Impl; + + thread Q + features + Data_Sink : in event data port Alpha_Type; + properties + Dispatch_Protocol => Sporadic; + Compute_Execution_Time => 1 ms .. 20 ms; + Priority => 2; + Period => 10 ms; + end Q; + + thread implementation Q.Impl + calls + Mycall : { + Q_Spg : subprogram Consume_Spg; + }; + connections + Z2:parameter Data_Sink -> Q_Spg.Data_Sink; + end Q.Impl; + + --------------- + -- Processor -- + --------------- + + processor the_processor + properties + Deployment::Execution_Platform => Native; + end the_processor; + + --------------- + -- Processes -- + --------------- + + process A + features + Alpha : out data port Alpha_Type; + end A; + + process implementation A.Impl + subcomponents + Producer : thread P.Impl; + connections + Z3:port Producer.Data_Source -> Alpha; + end A.Impl; + + process B + features + Beta : in data port Alpha_Type; + end B; + + process implementation B.Impl + subcomponents + Consumer : thread Q.Impl; + connections + Z4:port Beta -> Consumer.Data_Sink; + end B.Impl; + + ------------ + -- System -- + ------------ + + system PC_Simple + end PC_Simple; + + system implementation PC_Simple.Native + subcomponents + pr_A : process A.Impl; + pr_B : process B.Impl {Deployment::port_number => 4002;}; + Device_A : device Native_Sockets::Native_Sockets.pohic + {Source_Text => ("devicesconf.c");}; + Device_B : device Native_Sockets::Native_Sockets.pohic + {Source_Text => ("devicesconf.c");}; + + CPU_A : processor the_processor; + CPU_B : processor the_processor; + the_bus : bus Buses::Ethernet::Ethernet.impl; + connections + Z1: bus access the_bus -> Device_A.Eth; + Z2: bus access the_bus -> Device_B.Eth; + +-- Z5:bus access the_bus -> CPU.ETH; + Z6:port pr_A.Alpha -> pr_B.Beta; + properties + Actual_Processor_Binding => (reference (CPU_A)) applies to pr_A; + Actual_Processor_Binding => (reference (CPU_B)) applies to pr_B; + + Actual_Connection_Binding => (reference (the_bus)) applies to Z6; + actual_processor_binding => (reference (CPU_A)) applies to Device_A; + actual_processor_binding => (reference (CPU_B)) applies to Device_B; + + annex real_specification {** + theorem flow_latency + foreach s in system_set do + requires (Latency); + check (1=1); + end flow_latency; + **}; + end PC_Simple.Native; + +end Producer::Consumer;