Update examples file and upload expected final outputs per Benchmark

Updated examples directory. For each benchmark there is an assigned code indicating its Petri-Net class. The representation of files is as follows: <benchmark_name>_<ptnet_class_code> <class_code>: - MG = Marked Graph - FC = Free Choice - EFC = Extended Free Choice - AC = Asymmetric Choice - GN = General case Nets Also per each benchmark included expected output files and expected output command line log at 'msfsms_tool_bm.log' file.
workcraft · Dec 2, 2020 · 7eda28b · 7eda28b
1 parent ce28127
commit 7eda28b
Show file tree

Hide file tree

Showing 92 changed files with 21,705 additions and 31 deletions.
diff --git a/examples/5-dining-philosophers_GN/5-dining-philosophers.petrinet.GN.workcraft.g b/examples/5-dining-philosophers_GN/5-dining-philosophers.petrinet.GN.workcraft.g
@@ -0,0 +1,26 @@
+# STG file generated by Workcraft 3 (Return of the Hazard), version 3.2.0
+.model dining_philosophers_5
+.internal t0 t1 t2 t3 t4 t5 t6 t7 t9 t8
+.graph
+t0 p0 p2
+t1 p1
+t2 p2 p4
+t3 p3
+t4 p4 p6
+t5 p5
+t6 p6 p8
+t7 p7
+t9 p9
+t8 p0 p8
+p2 t1 t3
+p1 t0
+p0 t1 t9
+p4 t3 t5
+p3 t2
+p5 t4
+p6 t5 t7
+p8 t7 t9
+p7 t6
+p9 t8
+.marking {p1 p4 p7}
+.end
diff --git a/examples/5-dining-philosophers_GN/AsyncMSFSMs/fsm_afsm.afsm b/examples/5-dining-philosophers_GN/AsyncMSFSMs/fsm_afsm.afsm
@@ -0,0 +1,15 @@
+### FSMs' Declaration ###
+
+### Begin of FSM#01 Declaration ###
+p7*: t6_ p8
+p4*: t5_ p5
+p1*: t0_ p2
+p9: t8_ p0
+p6: t7_ p7
+p3: t2_ p4
+p0: t1_ p1
+p8: t9_ p9
+p5: t4_ p6
+p2: t3_ p3
+### End of FSM #01 Declaration ###
+
diff --git a/examples/5-dining-philosophers_GN/AsyncMSFSMs/msfsms_afsm.v b/examples/5-dining-philosophers_GN/AsyncMSFSMs/msfsms_afsm.v
@@ -0,0 +1,49 @@
+`timescale 1ns/1ns
+
+module msfsms_mealy (
+	clk,
+	data,
+	reset,
+	t9,
+	t6,
+	t3,
+	t0,
+	t8,
+	t5,
+	t2,
+	t7,
+	t4,
+	t1);
+
+	input reset;
+	input t9;
+	input t6;
+	input t3;
+	input t0;
+	input t8;
+	input t5;
+	input t2;
+	input t7;
+	input t4;
+	input t1;
+
+	wire p7_FSM1out, p4_FSM1out, p1_FSM1out, p9_FSM1out, p6_FSM1out, p3_FSM1out, p0_FSM1out, p8_FSM1out, p5_FSM1out, p2_FSM1out; // State Synchronisation output signals of FSM1 //
+
+
+	fsm_afsm_01 fsm_afsm_01_inst (
+		.sreset(reset)
+		.EN(clk)
+		.D(data),
+		.t9_(t9),
+		.t6_(t6),
+		.t3_(t3),
+		.t0_(t0),
+		.t8_(t8),
+		.t5_(t5),
+		.t2_(t2),
+		.t7_(t7),
+		.t4_(t4),
+		.t1_(t1)
+	);
+
+endmodule  // msfsms_mealy //
diff --git a/examples/5-dining-philosophers_GN/SyncMealyMSFSMs/fsm_behav_mealy.v b/examples/5-dining-philosophers_GN/SyncMealyMSFSMs/fsm_behav_mealy.v
@@ -0,0 +1,210 @@
+`timescale 1ns/1ns
+
+module fsm_mealy_behav_01 (
+	clk,
+	reset,
+	t9_,
+	t6_,
+	t3_,
+	t0_,
+	t8_,
+	t5_,
+	t2_,
+	t7_,
+	t4_,
+	t1_
+);
+
+	// Regular Synchronous FSM input Signals //
+	input clk;
+	input reset;
+
+	// Regular input Signals //
+	input t9_;
+	input t6_;
+	input t3_;
+	input t0_;
+	input t8_;
+	input t5_;
+	input t2_;
+	input t7_;
+	input t4_;
+	input t1_;
+	// Transition Barrier Inputs for input Signals //
+	// === EMPTY! === //
+
+	// Regular output Signals //
+	// === EMPTY! === //
+	// Transition Barrier outputs for output Signals //
+	// === EMPTY! === //
+
+	// FSMs' Synchronisation output Signals //
+	// === EMPTY! === //
+
+
+
+	parameter p7_1HOT_ENCODING = 10'd1; // 10'b0000000001 //
+	parameter p7_1HOT_CASEX_ENCODING = 10'bxxxxxxxxx1; // 10'b0000000001 //
+	parameter p4_1HOT_ENCODING = 10'd2; // 10'b0000000010 //
+	parameter p4_1HOT_CASEX_ENCODING = 10'bxxxxxxxx1x; // 10'b0000000010 //
+	parameter p1_1HOT_ENCODING = 10'd4; // 10'b0000000100 //
+	parameter p1_1HOT_CASEX_ENCODING = 10'bxxxxxxx1xx; // 10'b0000000100 //
+	parameter p9_1HOT_ENCODING = 10'd8; // 10'b0000001000 //
+	parameter p9_1HOT_CASEX_ENCODING = 10'bxxxxxx1xxx; // 10'b0000001000 //
+	parameter p6_1HOT_ENCODING = 10'd16; // 10'b0000010000 //
+	parameter p6_1HOT_CASEX_ENCODING = 10'bxxxxx1xxxx; // 10'b0000010000 //
+	parameter p3_1HOT_ENCODING = 10'd32; // 10'b0000100000 //
+	parameter p3_1HOT_CASEX_ENCODING = 10'bxxxx1xxxxx; // 10'b0000100000 //
+	parameter p0_1HOT_ENCODING = 10'd64; // 10'b0001000000 //
+	parameter p0_1HOT_CASEX_ENCODING = 10'bxxx1xxxxxx; // 10'b0001000000 //
+	parameter p8_1HOT_ENCODING = 10'd128; // 10'b0010000000 //
+	parameter p8_1HOT_CASEX_ENCODING = 10'bxx1xxxxxxx; // 10'b0010000000 //
+	parameter p5_1HOT_ENCODING = 10'd256; // 10'b0100000000 //
+	parameter p5_1HOT_CASEX_ENCODING = 10'bx1xxxxxxxx; // 10'b0100000000 //
+	parameter p2_1HOT_ENCODING = 10'd512; // 10'b1000000000 //
+	parameter p2_1HOT_CASEX_ENCODING = 10'b1xxxxxxxxx; // 10'b1000000000 //
+
+	reg [9 : 0]	state;
+	reg [9 : 0]	next_state;
+
+	always @(posedge clk)
+		begin
+			if (reset)
+				begin
+						// state <= p7_1HOT_ENCODING;
+						// state <= p4_1HOT_ENCODING;
+						// state <= p1_1HOT_ENCODING;
+						state[0] <= 1'b1;
+						state[1] <= 1'b1;
+						state[2] <= 1'b1;
+						state[3] <= 1'b0;
+						state[4] <= 1'b0;
+						state[5] <= 1'b0;
+						state[6] <= 1'b0;
+						state[7] <= 1'b0;
+						state[8] <= 1'b0;
+						state[9] <= 1'b0;
+				end
+			else
+				begin
+						state <= next_state;
+				end
+		end
+
+
+	always @(state or t9_ or t6_ or t3_ or t0_ or t8_ or t5_ or t2_ or t7_ or t4_ or t1_)
+		begin
+			// MEALY FSMs - Blocking Operations //
+			next_state = state;
+
+			// Empty output Events! //
+
+			casex (state)
+				10'bxxxxxxxxx1: // p7_1HOT_ENCODING: //
+					begin
+						if (t6_)
+							begin
+								// next_state = p8_1HOT_CASEX_ENCODING; //
+								next_state[0] = 1'b0;
+								next_state[7] = 1'b1;
+							end
+					end
+
+				10'bxxxxxxxx1x: // p4_1HOT_ENCODING: //
+					begin
+						if (t5_)
+							begin
+								// next_state = p5_1HOT_CASEX_ENCODING; //
+								next_state[1] = 1'b0;
+								next_state[8] = 1'b1;
+							end
+					end
+
+				10'bxxxxxxx1xx: // p1_1HOT_ENCODING: //
+					begin
+						if (t0_)
+							begin
+								// next_state = p2_1HOT_CASEX_ENCODING; //
+								next_state[2] = 1'b0;
+								next_state[9] = 1'b1;
+							end
+					end
+
+				10'bxxxxxx1xxx: // p9_1HOT_ENCODING: //
+					begin
+						if (t8_)
+							begin
+								// next_state = p0_1HOT_CASEX_ENCODING; //
+								next_state[3] = 1'b0;
+								next_state[6] = 1'b1;
+							end
+					end
+
+				10'bxxxxx1xxxx: // p6_1HOT_ENCODING: //
+					begin
+						if (t7_)
+							begin
+								// next_state = p7_1HOT_CASEX_ENCODING; //
+								next_state[4] = 1'b0;
+								next_state[0] = 1'b1;
+							end
+					end
+
+				10'bxxxx1xxxxx: // p3_1HOT_ENCODING: //
+					begin
+						if (t2_)
+							begin
+								// next_state = p4_1HOT_CASEX_ENCODING; //
+								next_state[5] = 1'b0;
+								next_state[1] = 1'b1;
+							end
+					end
+
+				10'bxxx1xxxxxx: // p0_1HOT_ENCODING: //
+					begin
+						if (t1_)
+							begin
+								// next_state = p1_1HOT_CASEX_ENCODING; //
+								next_state[6] = 1'b0;
+								next_state[2] = 1'b1;
+							end
+					end
+
+				10'bxx1xxxxxxx: // p8_1HOT_ENCODING: //
+					begin
+						if (t9_)
+							begin
+								// next_state = p9_1HOT_CASEX_ENCODING; //
+								next_state[7] = 1'b0;
+								next_state[3] = 1'b1;
+							end
+					end
+
+				10'bx1xxxxxxxx: // p5_1HOT_ENCODING: //
+					begin
+						if (t4_)
+							begin
+								// next_state = p6_1HOT_CASEX_ENCODING; //
+								next_state[8] = 1'b0;
+								next_state[4] = 1'b1;
+							end
+					end
+
+				10'b1xxxxxxxxx: // p2_1HOT_ENCODING: //
+					begin
+						if (t3_)
+							begin
+								// next_state = p3_1HOT_CASEX_ENCODING; //
+								next_state[9] = 1'b0;
+								next_state[5] = 1'b1;
+							end
+					end
+
+				default:
+						begin
+							next_state = 10'dx;
+						end
+			endcase
+		end
+endmodule
+