Shutters - Wake-up equations for Process-windows

This tool reads markings extension files (produced by a process windows mining tool), and generates the wakeup condition for each window, as well as the wakeup marking conditions for the places in each window. The tool uses espresso logic minimizer for synthesis of the obtained conditions. ABC can be also used optionally for their refactorisation.

How to install the tool

Clone the repository and run the Makefile.

$ git clone https://github.com/tuura/shutters.git # clone the repository
$ make # compile and build the tool

Run make help for displaying the Makefile commands.

How to use the tool

$ ./shutters [file.markings] -e [espresso_path]

Run ./shutters --help for the help of the tool.

Options available:
	-a ABC_path:		specify ABC path
	-e Espresso_path:	specify Espresso logic minimizer path
	-h or --help:		print help of the tool
	-p or --positive:	force equations to contain only positive literals
	-v or --version:	print tool version

Results

The following equations have been obtained by running the tool over the files contained inside the /test directory. buck.marking models the buck controller, the others are the FSMs depicted in the figures of the Process Windows article. Note: the places whose wakeup marking conditions are 0 are not shown for brevity. A place pN in window M is referred to as wMpN.

Motivational example

Negative literals without ABC	Positive literals without ABC	Negative literals with ABC	Positive literals with ABC
Marking eqs. win. 1: w1p0 = (w2p7); w1p2 = (!w2p7); w1p3 = 1;	Marking eqs. win. 1: w1p0 = (w2p7); w1p2 = (w2p6); w1p3 = 1;	Marking eqs. win. 1: w1p0 = w2p7; w1p2 = !w2p7; w1p3 = 1;	Marking eqs. win. 1: w1p0 = w2p7; w1p2 = w2p6; w1p3 = 1;
Marking eqs. win. 2: w2p6 = (!w1p0); w2p7 = (w1p0); w2p8 = 1;	Marking eqs. win. 2: w2p6 = (w1p2); w2p7 = (w1p0); w2p8 = 1;	Marking eqs. win. 2: w2p6 = !w1p0; w2p7 = w1p0; w2p8 = 1;	Marking eqs. win. 2: w2p6 = w1p2; w2p7 = w1p0; w2p8 = 1;
Eq. window 1: w1 = (w2p8*!w2p5);	Eq. window 1: w1 = (w2p6*w2p8) + (w2p8*w2p7);	Eq. window 1: w1 = !w2p5 * w2p8;	Eq. window 1: w1 = w2p8 * (w2p7 + w2p6);
Eq. window 2: w2 = (!w1p1*w1p3);	Eq. window 2: w2 = (w1p3*w1p2) + (w1p3*w1p0);	Eq. window 2: w2 = !w1p1 * w1p3;	Eq. window 2: w2 = w1p3 * (w1p0 + w1p2);

Arbiter

Negative literals without ABC	Positive literals without ABC	Negative literals with ABC	Positive literals with ABC
Marking eqs. win. 1: w1p0 = (!w2p9); w1p1 = (w2p9); w1p3 = 1;	Marking eqs. win. 1: w1p0 = (w2p8); w1p1 = (w2p9); w1p3 = 1;	Marking eqs. win. 1: w1p0 = !w2p9; w1p1 = w2p9; w1p3 = 1;	Marking eqs. win. 1: w1p0 = w2p8; w1p1 = w2p9; w1p3 = 1;
Marking eqs. win. 2: w2p5 = (!w1p4); w2p6 = (w1p4); w2p8 = 1;	Marking eqs. win. 2: w2p5 = (w1p3); w2p6 = (w1p4); w2p8 = 1;	Marking eqs. win. 2: w2p5 = !w1p4; w2p6 = w1p4; w2p8 = 1;	Marking eqs. win. 2: w2p5 = w1p3; w2p6 = w1p4; w2p8 = 1;
Eq. window 1: w1 = (w2p5);	Eq. window 1: w1 = (w2p5);	Eq. window 1: w1 = w2p5;	Eq. window 1: w1 = w2p5;
Eq. window 2: w2 = (w1p0);	Eq. window 2: w2 = (w1p0);	Eq. window 2: w2 = w1p0;	Eq. window 2: w2 = w1p0;

OR causality

Negative literals without ABC	Positive literals without ABC	Negative literals with ABC	Positive literals with ABC
Marking eqs. win. 1: w1.p0 = 1; w1.p3 = 1;	Marking eqs. win. 1: w1.p0 = 1; w1.p3 = 1;	Marking eqs. win. 1: w1.p0 = 1; w1.p3 = 1;	Marking eqs. win. 1: w1.p0 = 1; w1.p3 = 1;
Marking eqs. win. 2: w2.p5 = 1; w2.p8 = 1;	Marking eqs. win. 2: w2.p5 = 1; w2.p8 = 1;	Marking eqs. win. 2: w2.p5 = 1; w2.p8 = 1;	Marking eqs. win. 2: w2.p5 = 1; w2.p8 = 1;
Eq. window 1: w1 = (!w2.p9);	Eq. window 1: w1 = (w2.p8);	Eq. window 1: w1 = !w2.p9;	Eq. window 1: w1 = w2.p8;
Eq. window 2: w2 = (!w1.p4);	Eq. window 2: w2 = (w1.p3);	Eq. window 2: w2 = !w1.p4;	Eq. window 2: w2 = w1.p3;

Buck controller

Negative literals without ABC	Positive literals without ABC	Negative literals with ABC	Positive literals with ABC
Marking eqs. win. 1: w1.p1 = 1;	Marking eqs. win. 1: w1.p1 = 1;	Marking eqs. win. 1: w1.p1 = 1;	Marking eqs. win. 1: w1.p1 = 1;
Marking eqs. win. 2: w2.p1 = 1;	Marking eqs. win. 2: w2.p1 = 1;	Marking eqs. win. 2: w2.p1 = 1;	Marking eqs. win. 2: w2.p1 = 1;
Marking eqs. win. 3: w3.p3 = 1;	Marking eqs. win. 3: w3.p3 = 1;	Marking eqs. win. 3: w3.p3 = 1;	Marking eqs. win. 3: w3.p3 = 1;
Eq. window 1: w1 = (w2.p1*w3.p3);	Eq. window 1: w1 = (w2.p1*w3.p3);	Eq. window 1: w1 = w2.p1 * w3.p3;	Eq. window 1: w1 = w2.p1 * w3.p3;
Eq. window 2: w2 = (w1.p1*w3.p3);	Eq. window 2: w2 = (w1.p1*w3.p3);	Eq. window 2: w2 = w1.p1 * w3.p3;	Eq. window 2: w2 = w1.p1 * w3.p3;
Eq. window 3: w3 = (w1.p1*w2.p1);	Eq. window 3: w3 = (w1.p1*w2.p1);	Eq. window 3: w3 = w1.p1 * w2.p1;	Eq. window 3: w3 = w1.p1 * w2.p1;