Add wasm tacle-bench targets
This commit is contained in:
25
targets/wasm-tacle/sequential/petrinet/CMakeLists.txt
Normal file
25
targets/wasm-tacle/sequential/petrinet/CMakeLists.txt
Normal file
@ -0,0 +1,25 @@
|
||||
# ~~~
|
||||
# SPDX-License-Identifier: MIT
|
||||
# SPDX-FileCopyrightText: 2026, Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
|
||||
# ~~~
|
||||
|
||||
cmake_minimum_required(VERSION 3.20)
|
||||
|
||||
project(petrinet)
|
||||
|
||||
set(TACLEBENCH_ROOT_PATH "${CMAKE_CURRENT_LIST_DIR}/../../..")
|
||||
set(REPOSITORY_ROOT_PATH "${CMAKE_CURRENT_LIST_DIR}/../../../..")
|
||||
|
||||
set(APP_TARGET_NAME "${CMAKE_PROJECT_NAME}")
|
||||
|
||||
if(DEFINED TACLEBENCH_VARIANT AND "${TACLEBENCH_VARIANT}" STREQUAL "inline")
|
||||
set(APP_SOURCE_FILE_PATH
|
||||
"generated/modified_sources/inline/petrinet.c")
|
||||
else()
|
||||
set(APP_SOURCE_FILE_PATH
|
||||
"generated/modified_sources/default/petrinet.c")
|
||||
endif()
|
||||
|
||||
include(${REPOSITORY_ROOT_PATH}/cmake/taclebench_wasm.cmake)
|
||||
|
||||
|
||||
63
targets/wasm-tacle/sequential/petrinet/ChangeLog.txt
Executable file
63
targets/wasm-tacle/sequential/petrinet/ChangeLog.txt
Executable file
@ -0,0 +1,63 @@
|
||||
File: petrinet.c
|
||||
Original provenience: Mälardalen benchmark suite,
|
||||
http://www.mrtc.mdh.se/projects/wcet/wcet_bench/nsichneu/nsichneu.c
|
||||
|
||||
2016-02-02:
|
||||
- Added generic TACLeBench header.
|
||||
- Removed old file header (keep some information in TACLeBench
|
||||
header).
|
||||
- Renamed global variables:
|
||||
- main_iters_dummy_i -> petrinet_main_iters_dummy_i
|
||||
- main_min_dummy_i -> petrinet_main_min_dummy_i
|
||||
- main_max_dummy_i -> petrinet_main_max_dummy_i
|
||||
- P1_is_marked -> petrinet_P1_is_marked
|
||||
- P1_marking_member_0 -> petrinet_P1_marking_member_0
|
||||
- P2_is_marked -> petrinet_P2_is_marked
|
||||
- P2_marking_member_0 -> petrinet_P2_marking_member_0
|
||||
- P3_is_marked -> petrinet_P3_is_marked
|
||||
- P3_marking_member_0 -> petrinet_P3_marking_member_0
|
||||
- Renamed main function to petrinet_main, set as entrypoint.
|
||||
- Implemented new function main according to TACLeBench guidelines.
|
||||
- Implemented function petrinet_return, calculates checksum over
|
||||
petrinet_P3_marking_member_0.
|
||||
- Applied code formatting according to the following rules
|
||||
- Lines shall not be wider than 80 characters; whenever possible, appropriate
|
||||
line breaks shall be inserted to keep lines below 80 characters
|
||||
- Indentation is done using whitespaces only, no tabs. Code is indented by
|
||||
two whitespaces
|
||||
- Two empty lines are put between any two functions
|
||||
- In non-empty lists or index expressions, opening '(' and '[' are followed by
|
||||
one whitespace, closing ')' and ']' are preceded by one whitespace
|
||||
- In comma- or colon-separated argument lists, one whitespace is put after
|
||||
each comma/colon
|
||||
- Names of functions and global variables all start with a benchmark-specific
|
||||
prefix (here: bs_) followed by lowercase letter (e.g., bs_square)
|
||||
- For pointer types, one whitespace is put before the '*'
|
||||
- Operators within expressions shall be preceded and followed by one
|
||||
whitespace
|
||||
- Code of then- and else-parts of if-then-else statements shall be put in
|
||||
separate lines, not in the same lines as the if-condition or the keyword
|
||||
"else"
|
||||
- Opening braces '{' denoting the beginning of code for some if-else or loop
|
||||
body shall be put at the end of the same line where the keywords "if",
|
||||
"else", "for", "while" etc. occur
|
||||
- In non-empty lists or index expressions, opening '(' and '[' are followed by
|
||||
one whitespace, closing ')' and ']' are preceded by one whitespace
|
||||
- Operators within expressions shall be preceded and followed by one
|
||||
whitespace
|
||||
|
||||
2016-04-05:
|
||||
- Return '0' on success
|
||||
|
||||
2016-04-06:
|
||||
- Fixed generation of return value
|
||||
|
||||
2016-06-01:
|
||||
- Changed all prefixes to lower-case
|
||||
|
||||
2016-06-08:
|
||||
- Prefix
|
||||
- removed return from petrinet_main
|
||||
|
||||
2016-06-13:
|
||||
- introduced function petrinet_init
|
||||
BIN
targets/wasm-tacle/sequential/petrinet/generated/default/petrinet.wasm
Executable file
BIN
targets/wasm-tacle/sequential/petrinet/generated/default/petrinet.wasm
Executable file
Binary file not shown.
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,973 @@
|
||||
/*
|
||||
|
||||
This program is part of the TACLeBench benchmark suite.
|
||||
Version V 2.0
|
||||
|
||||
Name: Petrinet
|
||||
|
||||
Author: Friedhelm Stappert, C-LAB, Paderborn, Germany
|
||||
|
||||
Function: Simulate an extended Petri Net
|
||||
Automatically generated code containing large amounts of
|
||||
if-statements (more than 250)
|
||||
|
||||
Source: Mälardalen benchmark suite
|
||||
|
||||
Changes: no major functional changes
|
||||
|
||||
License: may be used, modified, and re-distributed freely
|
||||
|
||||
*/
|
||||
|
||||
/* Remove the following #define for actual WCET analyses! */
|
||||
/*
|
||||
#define PROFILING
|
||||
*/
|
||||
|
||||
// Wasm loop bounds
|
||||
|
||||
__attribute__((import_module("__pragma"), import_name("loopbound"))) extern void
|
||||
__pragma_loopbound(unsigned int min_bound, unsigned int max_bound);
|
||||
|
||||
#ifdef PROFILING
|
||||
#include <stdio.h>
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
/* Profiling variables. Remove for actual WCET analyses. */
|
||||
int petrinet_main_iters_dummy_i = 0, petrinet_main_min_dummy_i = 100000,
|
||||
petrinet_main_max_dummy_i = 0;
|
||||
#endif
|
||||
|
||||
/*
|
||||
Forward declaration of functions
|
||||
*/
|
||||
void petrinet_init(void);
|
||||
int petrinet_return(void);
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint"))) void
|
||||
petrinet_main(void);
|
||||
__attribute__((noinline)) __attribute__((export_name("main"))) int main(void);
|
||||
|
||||
volatile int petrinet_P1_is_marked;
|
||||
volatile long petrinet_P1_marking_member_0[3];
|
||||
volatile int petrinet_P2_is_marked;
|
||||
volatile long petrinet_P2_marking_member_0[5];
|
||||
volatile int petrinet_P3_is_marked;
|
||||
volatile long petrinet_P3_marking_member_0[6];
|
||||
|
||||
const long petrinet_CHECKSUM = 0;
|
||||
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint"))) void
|
||||
petrinet_main(void) {
|
||||
int dummy_i;
|
||||
/* dummy_i = 17; Takes too much time */
|
||||
dummy_i = 2;
|
||||
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i = 0;
|
||||
#endif
|
||||
__pragma_loopbound(2, 2);
|
||||
while (dummy_i > 0) {
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i++;
|
||||
#endif
|
||||
|
||||
dummy_i--;
|
||||
/* Permutation for Place P1 : 0, 1, 2 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[1] ==
|
||||
petrinet_P1_marking_member_0[2])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[0];
|
||||
y = petrinet_P1_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if (x < y) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 0, 2, 1 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[2] ==
|
||||
petrinet_P1_marking_member_0[1])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[0];
|
||||
y = petrinet_P1_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 0, 2 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[0] ==
|
||||
petrinet_P1_marking_member_0[2])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[1];
|
||||
y = petrinet_P1_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if (x < y) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 2, 0 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[2] ==
|
||||
petrinet_P1_marking_member_0[0])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[1];
|
||||
y = petrinet_P1_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 0, 1 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[0] ==
|
||||
petrinet_P1_marking_member_0[1])) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[2];
|
||||
y = petrinet_P1_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 1, 0 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[1] ==
|
||||
petrinet_P1_marking_member_0[0])) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[2];
|
||||
y = petrinet_P1_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place P2 : 0, 1, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
(((petrinet_P3_is_marked + 3) <= 6)) &&
|
||||
(((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[2])) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3])))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 1, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
(((petrinet_P3_is_marked + 3) <= 6)) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 0, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 2, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 0, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 1, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[3];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[3];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
}
|
||||
#ifdef PROFILING
|
||||
if (main_iters_dummy_i < main_min_dummy_i)
|
||||
main_min_dummy_i = main_iters_dummy_i;
|
||||
if (main_iters_dummy_i > main_max_dummy_i)
|
||||
main_max_dummy_i = main_iters_dummy_i;
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
printf("main::dummy_i-loop: [%d, %d]\n", main_min_dummy_i,
|
||||
main_max_dummy_i);
|
||||
#endif
|
||||
|
||||
// dummy_i = 77;
|
||||
// TODO: not a good return value
|
||||
// return dummy_i;
|
||||
}
|
||||
|
||||
void
|
||||
petrinet_init(void) {
|
||||
petrinet_P1_is_marked = 3;
|
||||
petrinet_P2_is_marked = 5;
|
||||
petrinet_P3_is_marked = 0;
|
||||
|
||||
/*
|
||||
Maybe we should also initialise these arrays, as they may be read
|
||||
in the petrinet_main() function before being written.
|
||||
*/
|
||||
/*
|
||||
volatile long petrinet_P1_marking_member_0[ 3 ];
|
||||
volatile long petrinet_P2_marking_member_0[ 5 ];
|
||||
volatile long petrinet_P3_marking_member_0[ 6 ];
|
||||
*/
|
||||
}
|
||||
|
||||
int
|
||||
petrinet_return(void) {
|
||||
// TODO: use something from the Px_... arrays
|
||||
int checksum = 0;
|
||||
int i;
|
||||
|
||||
__pragma_loopbound(3, 3);
|
||||
for (i = 0; i < 3; ++i)
|
||||
checksum += petrinet_P1_marking_member_0[i];
|
||||
|
||||
__pragma_loopbound(5, 5);
|
||||
for (i = 0; i < 5; ++i)
|
||||
checksum += petrinet_P2_marking_member_0[i];
|
||||
|
||||
__pragma_loopbound(6, 6);
|
||||
for (i = 0; i < 6; ++i)
|
||||
checksum += petrinet_P3_marking_member_0[i];
|
||||
|
||||
return ((checksum == petrinet_CHECKSUM) ? 0 : -1);
|
||||
}
|
||||
|
||||
__attribute__((noinline)) __attribute__((export_name("main"))) int
|
||||
main(void) {
|
||||
petrinet_main();
|
||||
|
||||
return (petrinet_return());
|
||||
}
|
||||
@ -0,0 +1,981 @@
|
||||
/*
|
||||
|
||||
This program is part of the TACLeBench benchmark suite.
|
||||
Version V 2.0
|
||||
|
||||
Name: Petrinet
|
||||
|
||||
Author: Friedhelm Stappert, C-LAB, Paderborn, Germany
|
||||
|
||||
Function: Simulate an extended Petri Net
|
||||
Automatically generated code containing large amounts of
|
||||
if-statements (more than 250)
|
||||
|
||||
Source: Mälardalen benchmark suite
|
||||
|
||||
Changes: no major functional changes
|
||||
|
||||
License: may be used, modified, and re-distributed freely
|
||||
|
||||
*/
|
||||
|
||||
/* Remove the following #define for actual WCET analyses! */
|
||||
/*
|
||||
#define PROFILING
|
||||
*/
|
||||
|
||||
// Wasm loop bounds
|
||||
|
||||
|
||||
|
||||
|
||||
__attribute__((import_module("__pragma"), import_name("loopbound"))) extern void
|
||||
__pragma_loopbound(unsigned int min_bound, unsigned int max_bound);
|
||||
|
||||
#ifdef PROFILING
|
||||
#include <stdio.h>
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
/* Profiling variables. Remove for actual WCET analyses. */
|
||||
int petrinet_main_iters_dummy_i = 0, petrinet_main_min_dummy_i = 100000,
|
||||
petrinet_main_max_dummy_i = 0;
|
||||
#endif
|
||||
|
||||
/*
|
||||
Forward declaration of functions
|
||||
*/
|
||||
__attribute__((always_inline)) static inline void petrinet_init(void);
|
||||
__attribute__((always_inline)) static inline int petrinet_return(void);
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint")))
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint"))) void
|
||||
petrinet_main(void);
|
||||
__attribute__((noinline)) __attribute__((export_name("main")))
|
||||
__attribute__((noinline)) __attribute__((export_name("main"))) int
|
||||
main(void);
|
||||
|
||||
volatile int petrinet_P1_is_marked;
|
||||
volatile long petrinet_P1_marking_member_0[3];
|
||||
volatile int petrinet_P2_is_marked;
|
||||
volatile long petrinet_P2_marking_member_0[5];
|
||||
volatile int petrinet_P3_is_marked;
|
||||
volatile long petrinet_P3_marking_member_0[6];
|
||||
|
||||
const long petrinet_CHECKSUM = 0;
|
||||
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint")))
|
||||
__attribute__((noinline)) __attribute__((export_name("entrypoint"))) void
|
||||
petrinet_main(void) {
|
||||
int dummy_i;
|
||||
/* dummy_i = 17; Takes too much time */
|
||||
dummy_i = 2;
|
||||
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i = 0;
|
||||
#endif
|
||||
__pragma_loopbound(2, 2);
|
||||
while (dummy_i > 0) {
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i++;
|
||||
#endif
|
||||
|
||||
dummy_i--;
|
||||
/* Permutation for Place P1 : 0, 1, 2 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[1] ==
|
||||
petrinet_P1_marking_member_0[2])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[0];
|
||||
y = petrinet_P1_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if (x < y) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 0, 2, 1 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[2] ==
|
||||
petrinet_P1_marking_member_0[1])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[0];
|
||||
y = petrinet_P1_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 0, 2 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[0] ==
|
||||
petrinet_P1_marking_member_0[2])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[1];
|
||||
y = petrinet_P1_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if (x < y) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 2, 0 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[2] ==
|
||||
petrinet_P1_marking_member_0[0])) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[1];
|
||||
y = petrinet_P1_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 0, 1 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[0] ==
|
||||
petrinet_P1_marking_member_0[1])) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[2];
|
||||
y = petrinet_P1_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 1, 0 */
|
||||
/* Transition T1 */
|
||||
if ((petrinet_P1_is_marked >= 3) && (petrinet_P3_is_marked + 3 <= 6) &&
|
||||
(petrinet_P1_marking_member_0[1] ==
|
||||
petrinet_P1_marking_member_0[0])) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[2];
|
||||
y = petrinet_P1_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((x < y)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = x;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = y;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place P2 : 0, 1, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
(((petrinet_P3_is_marked + 3) <= 6)) &&
|
||||
(((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[2])) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3])))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 1, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
(((petrinet_P3_is_marked + 3) <= 6)) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[0];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[2] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[2];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 0, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 2, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[1];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[3]) &&
|
||||
(petrinet_P2_marking_member_0[1] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[1];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 0, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 1, 0 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[3] ==
|
||||
petrinet_P2_marking_member_0[0]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[2];
|
||||
b = petrinet_P2_marking_member_0[3];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]))) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[3];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ((petrinet_P2_is_marked >= 4) &&
|
||||
((petrinet_P3_is_marked + 3) <= 6) &&
|
||||
((petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[2]) &&
|
||||
(petrinet_P2_marking_member_0[0] ==
|
||||
petrinet_P2_marking_member_0[1]))) {
|
||||
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[3];
|
||||
b = petrinet_P2_marking_member_0[0];
|
||||
|
||||
/* Transition condition */
|
||||
if ((b > a)) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 0] = a;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 1] = b;
|
||||
petrinet_P3_marking_member_0[petrinet_P3_is_marked + 2] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
}
|
||||
#ifdef PROFILING
|
||||
if (main_iters_dummy_i < main_min_dummy_i)
|
||||
main_min_dummy_i = main_iters_dummy_i;
|
||||
if (main_iters_dummy_i > main_max_dummy_i)
|
||||
main_max_dummy_i = main_iters_dummy_i;
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
printf("main::dummy_i-loop: [%d, %d]\n", main_min_dummy_i,
|
||||
main_max_dummy_i);
|
||||
#endif
|
||||
|
||||
// dummy_i = 77;
|
||||
// TODO: not a good return value
|
||||
// return dummy_i;
|
||||
}
|
||||
|
||||
__attribute__((always_inline)) static inline void
|
||||
petrinet_init(void) {
|
||||
petrinet_P1_is_marked = 3;
|
||||
petrinet_P2_is_marked = 5;
|
||||
petrinet_P3_is_marked = 0;
|
||||
|
||||
/*
|
||||
Maybe we should also initialise these arrays, as they may be read
|
||||
in the petrinet_main() function before being written.
|
||||
*/
|
||||
/*
|
||||
volatile long petrinet_P1_marking_member_0[ 3 ];
|
||||
volatile long petrinet_P2_marking_member_0[ 5 ];
|
||||
volatile long petrinet_P3_marking_member_0[ 6 ];
|
||||
*/
|
||||
}
|
||||
|
||||
__attribute__((always_inline)) static inline int
|
||||
petrinet_return(void) {
|
||||
// TODO: use something from the Px_... arrays
|
||||
int checksum = 0;
|
||||
int i;
|
||||
|
||||
__pragma_loopbound(3, 3);
|
||||
for (i = 0; i < 3; ++i)
|
||||
checksum += petrinet_P1_marking_member_0[i];
|
||||
|
||||
__pragma_loopbound(5, 5);
|
||||
for (i = 0; i < 5; ++i)
|
||||
checksum += petrinet_P2_marking_member_0[i];
|
||||
|
||||
__pragma_loopbound(6, 6);
|
||||
for (i = 0; i < 6; ++i)
|
||||
checksum += petrinet_P3_marking_member_0[i];
|
||||
|
||||
return ((checksum == petrinet_CHECKSUM) ? 0 : -1);
|
||||
}
|
||||
|
||||
__attribute__((noinline)) __attribute__((export_name("main")))
|
||||
__attribute__((noinline)) __attribute__((export_name("main"))) int
|
||||
main(void) {
|
||||
petrinet_main();
|
||||
|
||||
return (petrinet_return());
|
||||
}
|
||||
982
targets/wasm-tacle/sequential/petrinet/petrinet.c
Executable file
982
targets/wasm-tacle/sequential/petrinet/petrinet.c
Executable file
@ -0,0 +1,982 @@
|
||||
/*
|
||||
|
||||
This program is part of the TACLeBench benchmark suite.
|
||||
Version V 2.0
|
||||
|
||||
Name: Petrinet
|
||||
|
||||
Author: Friedhelm Stappert, C-LAB, Paderborn, Germany
|
||||
|
||||
Function: Simulate an extended Petri Net
|
||||
Automatically generated code containing large amounts of
|
||||
if-statements (more than 250)
|
||||
|
||||
Source: Mälardalen benchmark suite
|
||||
|
||||
Changes: no major functional changes
|
||||
|
||||
License: may be used, modified, and re-distributed freely
|
||||
|
||||
*/
|
||||
|
||||
/* Remove the following #define for actual WCET analyses! */
|
||||
/*
|
||||
#define PROFILING
|
||||
*/
|
||||
|
||||
#ifdef PROFILING
|
||||
#include <stdio.h>
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
/* Profiling variables. Remove for actual WCET analyses. */
|
||||
int petrinet_main_iters_dummy_i = 0,
|
||||
petrinet_main_min_dummy_i = 100000,
|
||||
petrinet_main_max_dummy_i = 0;
|
||||
#endif
|
||||
|
||||
/*
|
||||
Forward declaration of functions
|
||||
*/
|
||||
void petrinet_init( void );
|
||||
int petrinet_return( void );
|
||||
void petrinet_main( void );
|
||||
int main( void );
|
||||
|
||||
|
||||
volatile int petrinet_P1_is_marked;
|
||||
volatile long petrinet_P1_marking_member_0[ 3 ];
|
||||
volatile int petrinet_P2_is_marked;
|
||||
volatile long petrinet_P2_marking_member_0[ 5 ];
|
||||
volatile int petrinet_P3_is_marked;
|
||||
volatile long petrinet_P3_marking_member_0[ 6 ];
|
||||
|
||||
const long petrinet_CHECKSUM = 0;
|
||||
|
||||
void _Pragma ( "entrypoint" ) petrinet_main( void )
|
||||
{
|
||||
int dummy_i;
|
||||
/* dummy_i = 17; Takes too much time */
|
||||
dummy_i = 2;
|
||||
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i = 0;
|
||||
#endif
|
||||
_Pragma( "loopbound min 2 max 2" )
|
||||
while ( dummy_i > 0 ) {
|
||||
#ifdef PROFILING
|
||||
main_iters_dummy_i++;
|
||||
#endif
|
||||
|
||||
dummy_i--;
|
||||
/* Permutation for Place P1 : 0, 1, 2 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 1 ]
|
||||
== petrinet_P1_marking_member_0[ 2 ] ) ) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 0 ];
|
||||
y = petrinet_P1_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( x < y ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 0, 2, 1 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 2 ]
|
||||
== petrinet_P1_marking_member_0[ 1 ] ) ) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 0 ];
|
||||
y = petrinet_P1_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( x < y ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 0, 2 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 0 ]
|
||||
== petrinet_P1_marking_member_0[ 2 ] ) ) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 1 ];
|
||||
y = petrinet_P1_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( x < y ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 1, 2, 0 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 2 ]
|
||||
== petrinet_P1_marking_member_0[ 0 ] ) ) {
|
||||
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 1 ];
|
||||
y = petrinet_P1_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( x < y ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 0, 1 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 0 ]
|
||||
== petrinet_P1_marking_member_0[ 1 ] ) ) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 2 ];
|
||||
y = petrinet_P1_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( x < y ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P1 : 2, 1, 0 */
|
||||
/* Transition T1 */
|
||||
if ( ( petrinet_P1_is_marked >= 3 ) &&
|
||||
( petrinet_P3_is_marked + 3 <= 6 ) &&
|
||||
( petrinet_P1_marking_member_0[ 1 ]
|
||||
== petrinet_P1_marking_member_0[ 0 ] ) ) {
|
||||
long x;
|
||||
long y;
|
||||
long z;
|
||||
|
||||
x = petrinet_P1_marking_member_0[ 2 ];
|
||||
y = petrinet_P1_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( x < y ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P1_is_marked -= 3;
|
||||
|
||||
/* preaction */
|
||||
z = x - y;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = x;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = y;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = z;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place P2 : 0, 1, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( ( petrinet_P3_is_marked + 3 ) <= 6 ) ) &&
|
||||
( ( ( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 1, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( ( petrinet_P3_is_marked + 3 ) <= 6 ) ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 2, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 0, 3, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 0 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 2, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 0, 3, 2 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 2, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 2 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 2 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 0, 2 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 1, 3, 2, 0 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 1 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 1, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 0, 3, 1 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 0, 3 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 1, 3, 0 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 3 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 1 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 1 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 0, 1 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 2, 3, 1, 0 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 3 ]
|
||||
== petrinet_P2_marking_member_0[ 0 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 2 ];
|
||||
b = petrinet_P2_marking_member_0[ 3 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 1, 2 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) ) ) {
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 3 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
|
||||
|
||||
/* Permutation for Place petrinet_P2 : 3, 0, 2, 1 */
|
||||
/* Transition T2 */
|
||||
if ( ( petrinet_P2_is_marked >= 4 ) &&
|
||||
( ( petrinet_P3_is_marked + 3 ) <= 6 ) &&
|
||||
( ( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 2 ] ) &&
|
||||
( petrinet_P2_marking_member_0[ 0 ]
|
||||
== petrinet_P2_marking_member_0[ 1 ] ) ) ) {
|
||||
|
||||
long a;
|
||||
long b;
|
||||
long c;
|
||||
|
||||
a = petrinet_P2_marking_member_0[ 3 ];
|
||||
b = petrinet_P2_marking_member_0[ 0 ];
|
||||
|
||||
/* Transition condition */
|
||||
if ( ( b > a ) ) {
|
||||
|
||||
/* demarking of input places */
|
||||
petrinet_P2_is_marked -= 4;
|
||||
|
||||
/* preaction */
|
||||
c = a + b;
|
||||
|
||||
/* marking of output places */
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 0 ] = a;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 1 ] = b;
|
||||
petrinet_P3_marking_member_0[ petrinet_P3_is_marked + 2 ] = c;
|
||||
petrinet_P3_is_marked += 3;
|
||||
|
||||
} /* end of if (Transition condition) */
|
||||
}
|
||||
}
|
||||
#ifdef PROFILING
|
||||
if ( main_iters_dummy_i < main_min_dummy_i )
|
||||
main_min_dummy_i = main_iters_dummy_i;
|
||||
if ( main_iters_dummy_i > main_max_dummy_i )
|
||||
main_max_dummy_i = main_iters_dummy_i;
|
||||
#endif
|
||||
|
||||
#ifdef PROFILING
|
||||
printf( "main::dummy_i-loop: [%d, %d]\n",
|
||||
main_min_dummy_i, main_max_dummy_i );
|
||||
#endif
|
||||
|
||||
//dummy_i = 77;
|
||||
// TODO: not a good return value
|
||||
//return dummy_i;
|
||||
}
|
||||
|
||||
|
||||
void petrinet_init( void )
|
||||
{
|
||||
petrinet_P1_is_marked = 3;
|
||||
petrinet_P2_is_marked = 5;
|
||||
petrinet_P3_is_marked = 0;
|
||||
|
||||
/*
|
||||
Maybe we should also initialise these arrays, as they may be read
|
||||
in the petrinet_main() function before being written.
|
||||
*/
|
||||
/*
|
||||
volatile long petrinet_P1_marking_member_0[ 3 ];
|
||||
volatile long petrinet_P2_marking_member_0[ 5 ];
|
||||
volatile long petrinet_P3_marking_member_0[ 6 ];
|
||||
*/
|
||||
}
|
||||
|
||||
|
||||
int petrinet_return( void )
|
||||
{
|
||||
// TODO: use something from the Px_... arrays
|
||||
int checksum = 0;
|
||||
int i;
|
||||
|
||||
_Pragma( "loopbound min 3 max 3" )
|
||||
for ( i = 0; i < 3; ++i )
|
||||
checksum += petrinet_P1_marking_member_0[i];
|
||||
|
||||
_Pragma( "loopbound min 5 max 5" )
|
||||
for ( i = 0; i < 5; ++i )
|
||||
checksum += petrinet_P2_marking_member_0[i];
|
||||
|
||||
_Pragma( "loopbound min 6 max 6" )
|
||||
for ( i = 0; i < 6; ++i )
|
||||
checksum += petrinet_P3_marking_member_0[i];
|
||||
|
||||
return ( ( checksum == petrinet_CHECKSUM ) ? 0 : -1 );
|
||||
}
|
||||
|
||||
|
||||
int main( void )
|
||||
{
|
||||
petrinet_main();
|
||||
|
||||
return ( petrinet_return() );
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user