File	Date	Author	Commit
benchmark-e	2017-05-26	kslqq	[317b23] se-por for se-ltlx
benchmark-x	2017-05-26	kslqq	[317b23] se-por for se-ltlx
srcv0.0	2017-05-26	kslqq	[317b23] se-por for se-ltlx
README	2017-05-26	kslqq	[317b23] se-por for se-ltlx

Read Me

This SEX-SPIN model checker only partially supports the techniqe introduced in the paper:

     "Partial Order Reduction for the full Class of State/Event Linear Temporal Logic (SE-LTL)".


The file folder "benchmark-e" contains the experiments for SE-LTL without next operator

The file folder "benchmark-x" contains the experiments for SE-LTL with next operator 




For a formula $\phi$ to be verified, it is firstly translated into its negation $\neg \phi$.

The tool requires:
	
1. for any event literal l in a formula $\neg\phi$, which is a negation of an event, the predicate inst(\neg \phi,l)=true
2. all event-transitions are labeled with a conjunction of atomic propositions and events, no disjunction.
3. the generated pan.c file must be compiled with -DNOSTUTTER to disable stutter states.


In order to get sex-spin. in srcv0.0 folder and run make 



For the folder benchmark-3:


    Benchmark1 : Producer-Consumer

    Run the following Commands:


   	sex-spin -a pc.pr

   	gcc -DNOSTUTTER -o pan pan.c   //SE-LTL with POR
   
	gcc -DNOREDUCE -DNOSTUTTER -o pan pan.c // SE-LTL without POR

   	./pan -a

	You can change the numbers of producers and consumuers in the model "pc.pr"



    Benchmark2 : GIOP

    There are three models: giop1, giop2, giop3

    If we want to run giop1 then run the following Commands:

    cd ~/workspace/se-spin/benchmarks/GIOP*/giop1

    sex-spin -a giop1.nomig.pr 

    gcc -DNOSTUTTER -o pan pan.c  //SE-LTL with POR
   
    gcc -DNOSTUTTER -DNOREDUCE -o pan pan.c //SE-LTL without POR 

    ./pan -a




   In order to run spin model checker instead of se-spin model checker,
   you shoud run the following commands:

	spin -a giop1.spin.pr 

   	gcc -DNOSTUTTER -o pan pan.c  

	./pan -a

    For giop2 and giop3, they are same as giop1.

For folder benchmark-x:

    In each benchmark, 
    run the following commands:

    sex-spin -o3 -a *pr
    gcc -DNOSTUTTER -o pan pan.c
    ./pan -a