.clang-format

+---
+Language:        Cpp
+# BasedOnStyle:  LLVM
+AccessModifierOffset: -4
+AlignAfterOpenBracket: Align
+AlignConsecutiveAssignments: false
+AlignConsecutiveDeclarations: false
+AlignEscapedNewlines: Right
+AlignOperands:   true
+AlignTrailingComments: true
+AllowAllParametersOfDeclarationOnNextLine: false
+AllowShortBlocksOnASingleLine: true
+AllowShortCaseLabelsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: All
+AllowShortIfStatementsOnASingleLine: true
+AllowShortLoopsOnASingleLine: true
+AlwaysBreakAfterDefinitionReturnType: None
+AlwaysBreakAfterReturnType: None
+AlwaysBreakBeforeMultilineStrings: true
+AlwaysBreakTemplateDeclarations: MultiLine
+BinPackArguments: true
+BinPackParameters: true
+BraceWrapping:
+  AfterClass:      false
+  AfterControlStatement: false
+  AfterEnum:       false
+  AfterFunction:   false
+  AfterNamespace:  false
+  AfterObjCDeclaration: false
+  AfterStruct:     false
+  AfterUnion:      false
+  AfterExternBlock: false
+  BeforeCatch:     false
+  BeforeElse:      false
+  IndentBraces:    false
+  SplitEmptyFunction: false
+  SplitEmptyRecord: true
+  SplitEmptyNamespace: true
+BreakBeforeBinaryOperators: None
+BreakBeforeBraces: Attach
+BreakBeforeInheritanceComma: false
+BreakInheritanceList: BeforeColon
+BreakBeforeTernaryOperators: true
+BreakConstructorInitializersBeforeComma: false
+BreakConstructorInitializers: BeforeColon
+BreakAfterJavaFieldAnnotations: false
+BreakStringLiterals: true
+ColumnLimit:     0
+CommentPragmas:  '^ IWYU pragma:'
+CompactNamespaces: false
+ConstructorInitializerAllOnOneLineOrOnePerLine: false
+ConstructorInitializerIndentWidth: 4
+ContinuationIndentWidth: 8
+Cpp11BracedListStyle: true
+DerivePointerAlignment: false
+DisableFormat:   false
+ExperimentalAutoDetectBinPacking: false
+FixNamespaceComments: true
+ForEachMacros:
+  - foreach
+  - Q_FOREACH
+  - BOOST_FOREACH
+IncludeBlocks:   Preserve
+IncludeCategories:
+  - Regex:           '^"(llvm|llvm-c|clang|clang-c)/'
+    Priority:        2
+  - Regex:           '^(<|"(gtest|gmock|isl|json)/)'
+    Priority:        3
+  - Regex:           '.*'
+    Priority:        1
+IncludeIsMainRegex: '(Test)?$'
+IndentCaseLabels: true
+IndentPPDirectives: AfterHash
+IndentWidth:     4
+IndentWrappedFunctionNames: false
+JavaScriptQuotes: Leave
+JavaScriptWrapImports: true
+KeepEmptyLinesAtTheStartOfBlocks: true
+MacroBlockBegin: ''
+MacroBlockEnd:   ''
+MaxEmptyLinesToKeep: 2
+NamespaceIndentation: All
+ObjCBinPackProtocolList: Auto
+ObjCBlockIndentWidth: 2
+ObjCSpaceAfterProperty: false
+ObjCSpaceBeforeProtocolList: true
+PenaltyBreakAssignment: 2
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 300
+PenaltyBreakFirstLessLess: 120
+PenaltyBreakString: 1000
+PenaltyBreakTemplateDeclaration: 10
+PenaltyExcessCharacter: 1000000
+PenaltyReturnTypeOnItsOwnLine: 60
+PointerAlignment: Right
+ReflowComments:  false
+SortIncludes:    true
+SortUsingDeclarations: true
+SpaceAfterCStyleCast: false
+SpaceAfterTemplateKeyword: true
+SpaceBeforeAssignmentOperators: true
+SpaceBeforeCpp11BracedList: false
+SpaceBeforeCtorInitializerColon: true
+SpaceBeforeInheritanceColon: true
+SpaceBeforeParens: ControlStatements
+SpaceBeforeRangeBasedForLoopColon: true
+SpaceInEmptyParentheses: false
+SpacesBeforeTrailingComments: 0
+SpacesInAngles:  false
+SpacesInContainerLiterals: true
+SpacesInCStyleCastParentheses: false
+SpacesInParentheses: false
+SpacesInSquareBrackets: false
+Standard:        Cpp11
+TabWidth:        4
+UseTab:          Never
+...
+

Makefile

@@ -4,84 +4,43 @@
 CC		= g++
 #CC        = g++-10
 
-#CXXFLAGS		= -Wall -Wextra -std=c++11 -Wfatal-errors
-CXXFLAGS 		= -Wall -Wextra -std=c++11 -Wfatal-errors -g
-#CXXFLAGS		= -Wall -Wextra -std=c++11 -O3 
-#CXXFLAGS		= -Wall -Wextra -std=c++11 -Wfatal-errors -O1
+#CXX_FLAGS		= -Wall -Wextra -std=c++11 -Wfatal-errors
+CXX_FLAGS 		= -Wall -Wextra -std=c++11 -Wfatal-errors -g
+#CXX_FLAGS		= -Wall -Wextra -std=c++11 -O3
+#CXX_FLAGS		= -Wall -Wextra -std=c++11 -Wfatal-errors -O1
 
-# 
-# linker flags
 #
-#LDFLAGS			= -ldl -lomp
-LDFLAGS			= -ldl
-
-#
-# fairsyn 
-#
-FAIRSYNROOT		= .
-FAIRSYNINC		= -I$(FAIRSYNROOT) -I$(FAIRSYNROOT)/utils -I$(FAIRSYNROOT)/lib 
-
-#
-# src folder
-#
-FAIRSYNSRC		= $(FAIRSYNROOT)/src
-
-#
-# bin folder
-#
-FAIRSYNBIN		= $(FAIRSYNROOT)/bin
-MKDIR_P			= mkdir -p
-
-#
-# sylvan
-#
-
-#SYLVANPATH		= /usr/local
-SYLVANPATH		= ../../libraries/
-SYLVANINC		= -I$(SYLVANPATH)/include/
-SYLVANLIB		= -L$(SYLVANPATH)/lib -lsylvan
-
+# Targets
 #
-# hoaf library
-#
-
-#HOAFLIBPATH	= /opt/local/include
-#HOAFLIBPATH	= /opt/local/include/cpphoafparser
-#HOAFLIBPATH	= /home/tamajit/Desktop/HOAF/include
-HOAFLIBPATH	= /home/tbanerjee/library/cpphoafparser-0.99.2/include
-#HOAFINC		= -isystem $(HOAFLIBPATH)/ast -isystem $(HOAFLIBPATH)/consumer -isystem $(HOAFLIBPATH)/parser
-HOAFINC		= -isystem $(HOAFLIBPATH)
-
-TARGETF = $(FAIRSYNBIN)/main_fairsyn
-
-TARGETS = $(FAIRSYNBIN)/general_queue
 
+TARGET_F = $(FAIRSYN_BIN)/main_fairsyn
+TARGET_S = $(FAIRSYN_BIN)/general_queue
 
 #
 # object files
 #
 
-OBJF    = $(TARGETF).o
-OBJS    = $(TARGETS).o
+OBJF    = $(TARGET_F).o
+OBJS    = $(TARGET_S).o
 
 .PHONY: directories
 
-all: directories $(TARGETF) $(TARGETS) $(TARGETG) $(TARGETGN) $(DEBUGF)
+all: directories $(TARGET_F) $(TARGET_S) $(TARGET_G) $(TARGET_GN) $(DEBUG_F)
 
-directories: $(FAIRSYNBIN)
+directories: $(FAIRSYN_BIN)
 
-$(FAIRSYNBIN):
-	$(MKDIR_P) $(FAIRSYNBIN)
+$(FAIRSYN_BIN):
+	$(MKDIR_P) $(FAIRSYN_BIN)
 
-$(FAIRSYNBIN)/%.o:$(FAIRSYNSRC)/%.cc
-	$(CC) -c -o $@ $< $(CXXFLAGS) $(HOAFINC) $(SYLVANINC) $(FAIRSYNINC) 
+$(FAIRSYN_BIN)/%.o:$(FAIRSYN_SRC)/%.cc
+	$(CC) -c -o $@ $< $(CXX_FLAGS) $(HOAF_INC) $(SYLVAN_INC) $(FAIRSYN_INC)
 
-$(TARGETF): $(OBJF)
-	$(CC) $(CXXFLAGS) -o $@ $^ $(LDFLAGS) $(SYLVANLIB)
+$(TARGET_F): $(OBJF)
+	$(CC) $(CXX_FLAGS) -o $@ $^ $(LD_FLAGS) $(SYLVAN_LIB)
 	
 
-$(TARGETS): $(OBJS)
-	$(CC) $(CXXFLAGS) -o $@ $^ $(LDFLAGS) $(SYLVANLIB)
+$(TARGET_S): $(OBJS)
+	$(CC) $(CXX_FLAGS) -o $@ $^ $(LD_FLAGS) $(SYLVAN_LIB)
 
 clean:
-	rm  $(TARGETS)  $(TARGETS).o $(TARGETF)  $(TARGETF).o
+	rm  $(TARGET_S)  $(TARGET_S).o $(TARGET_F)  $(TARGET_F).o

README.md

 # synthesis-with-edge-fairness
 
-Parallel reactive synthesis for omega-regular specifications under the transition fairness condition
\ No newline at end of file
+Parallel reactive synthesis for omega-regular specifications under the transition fairness condition
+
+
+1.  Install clang-format to maintain code style
+    for Mac OS use
+
+        brew install clang-format.
+
+    and for Linux use
+
+        sudo apt-get install clang-format
+
+    To reform file run:
+
+        clang-format -i /path/to/file.cc
+
+    or run formatting in your editor:
+
+    -   Clion:  `Ctrl` + `Shift` + `Alt` + `L`
+    -   XCode:  Select text (`Cmd` + `A`) and then `Ctrl` + `I`.
+    -   Atom: After saving
+    -   VSCode: `CTRL` +`R` or `CTRL` + `D`
+
+Setup Environment
+================
+
+You need to create a copy of `template_env.sh` and name it `env.sh`.
+Open `env.sh` and change the paths to first a few environment variables (it's best to use absolute paths).
+Every time you open a terminal you need to run:
+
+    source env.sh
+
+or this command can be added (with proper path) into the ~/.bashrc file so
+that the path is automatically loaded each time.
+
+TACAS '22 Artifact
+==================
+
+You can obtain the draft of our TACAS '22 submission along with the artifact in this [link](https://calendar.mpi-sws.org/index.php/s/ALDTtcJHZRezpq6). We tested the artifact on the [virtual machine](https://zenodo.org/record/5562597#.YYULqSUo_mE) provided by the TACAS '22 AE Committee. To generate the results, you need to simply extract the TACAS_AE_Archive.zip file within the virtual machine, and then follow the instructions provided in the Readme.txt file.

bcg/other_codes/Convert.cpp

-#include <iostream>
 #include <fstream>
+#include <iostream>
 #include <string>
 using namespace std;
-int main(){
-	fstream newfile;
-	//cout<<"hi\n";
-	newfile.open("cwi_1_2.txt",ios::in);
-	int n;
-	newfile>>n;
-	cout<<n<<"\n";
-	while(n--){
-	int num;
-	newfile>>num;
-	while(num!=-1){
-	cout<<num<<" ";
-	newfile>>num;
-	}	
-	cout<<"\n";
-	}
-	newfile.close();
-	return 0;
+int main() {
+    fstream newfile;
+    //cout<<"hi\n";
+    newfile.open("cwi_1_2.txt", ios::in);
+    int n;
+    newfile >> n;
+    cout << n << "\n";
+    while (n--) {
+        int num;
+        newfile >> num;
+        while (num != -1) {
+            cout << num << " ";
+            newfile >> num;
+        }
+        cout << "\n";
+    }
+    newfile.close();
+    return 0;
 }

bcg/other_codes/Experiment.c

 #include "bcg_user.h"
 
 /* The following function prints information about a BCG graph */
-void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph)
-{
-   printf ("initial state = %lu\n", BCG_OT_INITIAL_STATE (bcg_graph));
-   printf ("nb states = %lu\n", BCG_OT_NB_STATES (bcg_graph));
-   printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph));
-   printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
+void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
+    printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(bcg_graph));
+    printf("nb states = %lu\n", BCG_OT_NB_STATES(bcg_graph));
+    printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
+    printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
 }
 
 /* The following function displays an edge */
 
-void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBER bcg_state_1 , BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2 )
-{
-   BCG_TYPE_C_STRING bcg_label_string;
-   BCG_TYPE_BOOLEAN bcg_visible;
-   BCG_TYPE_NATURAL bcg_cardinal;
-   BCG_TYPE_C_STRING bcg_gate;
+void bcg_print_edge(BCG_TYPE_OBJECT_TRANSITION bcg_graph, BCG_TYPE_STATE_NUMBER bcg_state_1,
+                    BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2) {
+    BCG_TYPE_C_STRING bcg_label_string;
+    BCG_TYPE_BOOLEAN bcg_visible;
+    BCG_TYPE_NATURAL bcg_cardinal;
+    BCG_TYPE_C_STRING bcg_gate;
 
-   bcg_label_string = BCG_OT_LABEL_STRING (bcg_graph, bcg_label_number);
-   bcg_visible = BCG_OT_LABEL_VISIBLE (bcg_graph, bcg_label_number);
-   bcg_cardinal = BCG_OT_LABEL_CARDINAL (bcg_graph, bcg_label_number);
+    bcg_label_string = BCG_OT_LABEL_STRING(bcg_graph, bcg_label_number);
+    bcg_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
+    bcg_cardinal = BCG_OT_LABEL_CARDINAL(bcg_graph, bcg_label_number);
 
-   printf ("transition from state %lu to state %lu\n", 
+    printf("transition from state %lu to state %lu\n",
            bcg_state_1, bcg_state_2);
-   printf ("label unique number = %u\n", bcg_label_number);
-   printf ("label string = %s\n", bcg_label_string);
-   printf ("label cardinal = %u\n", bcg_cardinal);
-   if (bcg_visible) {
-      bcg_gate = BCG_OT_LABEL_GATE (bcg_graph, bcg_label_number);
-      printf ("visible label (gate = %s)\n", bcg_gate);
-   } else {
-      bcg_gate = BCG_OT_LABEL_HIDDEN_GATE (bcg_graph, bcg_label_number);
-      printf ("hidden label (hidden gate = %s)\n", bcg_gate);
-   }
+    printf("label unique number = %u\n", bcg_label_number);
+    printf("label string = %s\n", bcg_label_string);
+    printf("label cardinal = %u\n", bcg_cardinal);
+    if (bcg_visible) {
+        bcg_gate = BCG_OT_LABEL_GATE(bcg_graph, bcg_label_number);
+        printf("visible label (gate = %s)\n", bcg_gate);
+    } else {
+        bcg_gate = BCG_OT_LABEL_HIDDEN_GATE(bcg_graph, bcg_label_number);
+        printf("hidden label (hidden gate = %s)\n", bcg_gate);
+    }
 }
 
 
-int main ()
-{
-   BCG_TYPE_OBJECT_TRANSITION bcg_graph;
-   BCG_TYPE_STATE_NUMBER bcg_s1;
-   BCG_TYPE_LABEL_NUMBER bcg_label_number;
-   BCG_TYPE_STATE_NUMBER bcg_s2;
-   BCG_TYPE_STATE_NUMBER bcg_nb_states;
-   BCG_TYPE_C_STRING bcg_label_string;
+int main() {
+    BCG_TYPE_OBJECT_TRANSITION bcg_graph;
+    BCG_TYPE_STATE_NUMBER bcg_s1;
+    BCG_TYPE_LABEL_NUMBER bcg_label_number;
+    BCG_TYPE_STATE_NUMBER bcg_s2;
+    BCG_TYPE_STATE_NUMBER bcg_nb_states;
+    BCG_TYPE_C_STRING bcg_label_string;
 
-   BCG_INIT ();
+    BCG_INIT();
 
 
-   BCG_OT_READ_BCG_BEGIN ("vasy_0_1.bcg", &bcg_graph, 0);
-   bcg_print_info (bcg_graph);
-   
-   for(int i=0;i< BCG_OT_NB_LABELS(bcg_graph);i++){
-   bcg_label_string = BCG_OT_LABEL_STRING (bcg_graph, i );
-   	 printf ("label string = %s\n", bcg_label_string);
-   }
+    BCG_OT_READ_BCG_BEGIN("vasy_0_1.bcg", &bcg_graph, 0);
+    bcg_print_info(bcg_graph);
 
+    for (int i = 0; i < BCG_OT_NB_LABELS(bcg_graph); i++) {
+        bcg_label_string = BCG_OT_LABEL_STRING(bcg_graph, i);
+        printf("label string = %s\n", bcg_label_string);
+    }
 
-   
-   BCG_OT_READ_BCG_END (&bcg_graph);
-   exit (0);
+
+    BCG_OT_READ_BCG_END(&bcg_graph);
+    exit(0);
 }

bcg/other_codes/Read.c

 #include "bcg_user.h"
 
 /* The following function prints information about a BCG graph */
-void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph)
-{
-   printf ("initial state = %lu\n", BCG_OT_INITIAL_STATE (bcg_graph));
-   printf ("nb states = %lu\n", BCG_OT_NB_STATES (bcg_graph));
-   printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph));
-   printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
+void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
+    printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(bcg_graph));
+    printf("nb states = %lu\n", BCG_OT_NB_STATES(bcg_graph));
+    printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
+    printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
 }
 
 /* The following function displays an edge */
 
-void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBER bcg_state_1 , BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2 )
-{
-   BCG_TYPE_C_STRING bcg_label_string;
-   BCG_TYPE_BOOLEAN bcg_visible;
-   BCG_TYPE_NATURAL bcg_cardinal;
-   BCG_TYPE_C_STRING bcg_gate;
+void bcg_print_edge(BCG_TYPE_OBJECT_TRANSITION bcg_graph, BCG_TYPE_STATE_NUMBER bcg_state_1, BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2) {
+    BCG_TYPE_C_STRING bcg_label_string;
+    BCG_TYPE_BOOLEAN bcg_visible;
+    BCG_TYPE_NATURAL bcg_cardinal;
+    BCG_TYPE_C_STRING bcg_gate;
 
-   bcg_label_string = BCG_OT_LABEL_STRING (bcg_graph, bcg_label_number);
-   bcg_visible = BCG_OT_LABEL_VISIBLE (bcg_graph, bcg_label_number);
-   bcg_cardinal = BCG_OT_LABEL_CARDINAL (bcg_graph, bcg_label_number);
+    bcg_label_string = BCG_OT_LABEL_STRING(bcg_graph, bcg_label_number);
+    bcg_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
+    bcg_cardinal = BCG_OT_LABEL_CARDINAL(bcg_graph, bcg_label_number);
 
-   printf ("transition from state %lu to state %lu\n", 
+    printf("transition from state %lu to state %lu\n",
            bcg_state_1, bcg_state_2);
-   printf ("label unique number = %u\n", bcg_label_number);
-   printf ("label string = %s\n", bcg_label_string);
-   printf ("label cardinal = %u\n", bcg_cardinal);
-   if (bcg_visible) {
-      bcg_gate = BCG_OT_LABEL_GATE (bcg_graph, bcg_label_number);
-      printf ("visible label (gate = %s)\n", bcg_gate);
-   } else {
-      bcg_gate = BCG_OT_LABEL_HIDDEN_GATE (bcg_graph, bcg_label_number);
-      printf ("hidden label (hidden gate = %s)\n", bcg_gate);
-   }
+    printf("label unique number = %u\n", bcg_label_number);
+    printf("label string = %s\n", bcg_label_string);
+    printf("label cardinal = %u\n", bcg_cardinal);
+    if (bcg_visible) {
+        bcg_gate = BCG_OT_LABEL_GATE(bcg_graph, bcg_label_number);
+        printf("visible label (gate = %s)\n", bcg_gate);
+    } else {
+        bcg_gate = BCG_OT_LABEL_HIDDEN_GATE(bcg_graph, bcg_label_number);
+        printf("hidden label (hidden gate = %s)\n", bcg_gate);
+    }
 }
 
 
-int main ()
-{
-   BCG_TYPE_OBJECT_TRANSITION bcg_graph;
-   BCG_TYPE_STATE_NUMBER bcg_s1;
-   BCG_TYPE_LABEL_NUMBER bcg_label_number;
-   BCG_TYPE_STATE_NUMBER bcg_s2;
-   BCG_TYPE_STATE_NUMBER bcg_nb_states;
+int main() {
+    BCG_TYPE_OBJECT_TRANSITION bcg_graph;
+    BCG_TYPE_STATE_NUMBER bcg_s1;
+    BCG_TYPE_LABEL_NUMBER bcg_label_number;
+    BCG_TYPE_STATE_NUMBER bcg_s2;
+    BCG_TYPE_STATE_NUMBER bcg_nb_states;
 
-   BCG_INIT ();
+    BCG_INIT();
 
 
+    BCG_OT_READ_BCG_BEGIN("vasy_0_1.bcg", &bcg_graph, 0);
+    bcg_print_info(bcg_graph);
+    BCG_OT_ITERATE_PLN(bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
+        bcg_print_edge(bcg_graph, bcg_s1, bcg_label_number, bcg_s2);
+    }
+    BCG_OT_END_ITERATE;
 
-   BCG_OT_READ_BCG_BEGIN ("vasy_0_1.bcg", &bcg_graph, 0);
-   bcg_print_info (bcg_graph);
-   BCG_OT_ITERATE_PLN (bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
-      bcg_print_edge (bcg_graph, bcg_s1, bcg_label_number, bcg_s2);
-   } BCG_OT_END_ITERATE;
-   
-   BCG_OT_READ_BCG_END (&bcg_graph);
-   BCG_OT_READ_BCG_BEGIN ("vasy_0_1.bcg", &bcg_graph, 1);
-   bcg_print_info (bcg_graph);
-   bcg_nb_states = BCG_OT_NB_STATES (bcg_graph);
-   for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
-      printf ("successors of state %lu:\n", bcg_s1);
-      BCG_OT_ITERATE_P_LN (bcg_graph, bcg_s1, bcg_label_number, bcg_s2)
-{
-        bcg_print_edge (bcg_graph, bcg_s1, bcg_label_number, bcg_s2);
-      } BCG_OT_END_ITERATE;
-   }
-   BCG_OT_READ_BCG_END (&bcg_graph);
-   exit (0);
+    BCG_OT_READ_BCG_END(&bcg_graph);
+    BCG_OT_READ_BCG_BEGIN("vasy_0_1.bcg", &bcg_graph, 1);
+    bcg_print_info(bcg_graph);
+    bcg_nb_states = BCG_OT_NB_STATES(bcg_graph);
+    for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
+        printf("successors of state %lu:\n", bcg_s1);
+        BCG_OT_ITERATE_P_LN(bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
+            bcg_print_edge(bcg_graph, bcg_s1, bcg_label_number, bcg_s2);
+        }
+        BCG_OT_END_ITERATE;
+    }
+    BCG_OT_READ_BCG_END(&bcg_graph);
+    exit(0);
 }

bcg/other_codes/Write.c

 #include "bcg_user.h"
-int main ()
-{
-   BCG_TYPE_STATE_NUMBER S1;
-   BCG_TYPE_LABEL_STRING L = "";
-   BCG_TYPE_STATE_NUMBER S2;
-   BCG_INIT ();
-   BCG_IO_WRITE_BCG_BEGIN ("test.bcg", 0, 2, "created by tool", 1);
-   for(int i=0;i<10;i++)
-   {
-   	 		S1 = i;
-   	for(int j=i+1;j<10;j++){
- 			S2 = j;
-   		BCG_IO_WRITE_BCG_EDGE (S1, L , S2);
-   	}
-   }
-   BCG_IO_WRITE_BCG_END ();
-   return (0);
+int main() {
+    BCG_TYPE_STATE_NUMBER S1;
+    BCG_TYPE_LABEL_STRING L = "";
+    BCG_TYPE_STATE_NUMBER S2;
+    BCG_INIT();
+    BCG_IO_WRITE_BCG_BEGIN("test.bcg", 0, 2, "created by tool", 1);
+    for (int i = 0; i < 10; i++) {
+        S1 = i;
+        for (int j = i + 1; j < 10; j++) {
+            S2 = j;
+            BCG_IO_WRITE_BCG_EDGE(S1, L, S2);
+        }
+    }
+    BCG_IO_WRITE_BCG_END();
+    return (0);
 }

bcg/src/Extraction.c

 #include "bcg_user.h"
 
 /* The following function prints information about a BCG graph */
-void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph)
-{
-   printf ("initial state = %lu\n", BCG_OT_INITIAL_STATE (bcg_graph));
-   printf ("nb states = %lu\n", BCG_OT_NB_STATES (bcg_graph));
-   printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph));
-   printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
+void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
+    printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(bcg_graph));
+    printf("nb states = %lu\n", BCG_OT_NB_STATES(bcg_graph));
+    printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
+    printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
 }
 
 /* The following function displays an edge */
 
-void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBER bcg_state_1 , BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2 )
-{
-   BCG_TYPE_C_STRING bcg_label_string;
-   BCG_TYPE_BOOLEAN bcg_visible;
-   BCG_TYPE_NATURAL bcg_cardinal;
-   BCG_TYPE_C_STRING bcg_gate;
+void bcg_print_edge(BCG_TYPE_OBJECT_TRANSITION bcg_graph, BCG_TYPE_STATE_NUMBER bcg_state_1, BCG_TYPE_LABEL_NUMBER bcg_label_number, BCG_TYPE_STATE_NUMBER bcg_state_2) {
+    BCG_TYPE_C_STRING bcg_label_string;
+    BCG_TYPE_BOOLEAN bcg_visible;
+    BCG_TYPE_NATURAL bcg_cardinal;
+    BCG_TYPE_C_STRING bcg_gate;
 
-   bcg_label_string = BCG_OT_LABEL_STRING (bcg_graph, bcg_label_number);
-   bcg_visible = BCG_OT_LABEL_VISIBLE (bcg_graph, bcg_label_number);
-   bcg_cardinal = BCG_OT_LABEL_CARDINAL (bcg_graph, bcg_label_number);
+    bcg_label_string = BCG_OT_LABEL_STRING(bcg_graph, bcg_label_number);
+    bcg_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
+    bcg_cardinal = BCG_OT_LABEL_CARDINAL(bcg_graph, bcg_label_number);
 
-   fprintf ("transition from state %lu to state %lu\n", 
-           bcg_state_1, bcg_state_2);
-   /*printf ("label unique number = %u\n", bcg_label_number);
+    fprintf("transition from state %lu to state %lu\n",
+            bcg_state_1, bcg_state_2);
+    /*printf ("label unique number = %u\n", bcg_label_number);
    printf ("label string = %s\n", bcg_label_string);
    printf ("label cardinal = %u\n", bcg_cardinal);
    if (bcg_visible) {
@@ -37,61 +35,60 @@ void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBE
 }
 
 
-int main (int argc, char *argv[])
-{
-   FILE *fptr;
-    char * file_path1 = "../output/";
-    char * file_path2 = "../input/";
-    char * file_extention1 = ".txt";
-    char * file_extention2 = ".bcg";
-    
+int main(int argc, char *argv[]) {
+    FILE *fptr;
+    char *file_path1 = "../output/";
+    char *file_path2 = "../input/";
+    char *file_extention1 = ".txt";
+    char *file_extention2 = ".bcg";
+
     int size_fileopen = strlen(argv[1]) + strlen(file_path1) + strlen(file_extention1) + 1;
-    char * fileopen = (char *)malloc(size_fileopen);
-    strcpy(fileopen , file_path1);
-    strcat(fileopen , argv[1]);
-    strcat(fileopen , file_extention1);
-    fptr =fopen(fileopen,"w");
-   
-   BCG_TYPE_OBJECT_TRANSITION bcg_graph;
-   BCG_TYPE_STATE_NUMBER bcg_s1;
-   BCG_TYPE_LABEL_NUMBER bcg_label_number;
-   BCG_TYPE_STATE_NUMBER bcg_s2;
-   BCG_TYPE_STATE_NUMBER bcg_nb_states;
-
-	
-   int size_bcgopen = strlen(argv[1]) + strlen(file_path2) + strlen(file_extention2) + 1;
-    char * bcgopen = (char *)malloc(size_bcgopen);
-    strcpy(bcgopen , file_path2);
-    strcat(bcgopen , argv[1]);
-    strcat(bcgopen , file_extention2);
-    
-   BCG_INIT ();
-   BCG_OT_READ_BCG_BEGIN (bcgopen, &bcg_graph, 1);
-   int initial_state = BCG_OT_INITIAL_STATE (bcg_graph);
-   int number_of_states = BCG_OT_NB_STATES (bcg_graph);
-   int number_of_edges =  BCG_OT_NB_EDGES (bcg_graph);
-   
-   fprintf(fptr,"%lu\n",number_of_states);
-   
-   /*
+    char *fileopen = (char *)malloc(size_fileopen);
+    strcpy(fileopen, file_path1);
+    strcat(fileopen, argv[1]);
+    strcat(fileopen, file_extention1);
+    fptr = fopen(fileopen, "w");
+
+    BCG_TYPE_OBJECT_TRANSITION bcg_graph;
+    BCG_TYPE_STATE_NUMBER bcg_s1;
+    BCG_TYPE_LABEL_NUMBER bcg_label_number;
+    BCG_TYPE_STATE_NUMBER bcg_s2;
+    BCG_TYPE_STATE_NUMBER bcg_nb_states;
+
+
+    int size_bcgopen = strlen(argv[1]) + strlen(file_path2) + strlen(file_extention2) + 1;
+    char *bcgopen = (char *)malloc(size_bcgopen);
+    strcpy(bcgopen, file_path2);
+    strcat(bcgopen, argv[1]);
+    strcat(bcgopen, file_extention2);
+
+    BCG_INIT();
+    BCG_OT_READ_BCG_BEGIN(bcgopen, &bcg_graph, 1);
+    int initial_state = BCG_OT_INITIAL_STATE(bcg_graph);
+    int number_of_states = BCG_OT_NB_STATES(bcg_graph);
+    int number_of_edges = BCG_OT_NB_EDGES(bcg_graph);
+
+    fprintf(fptr, "%lu\n", number_of_states);
+
+    /*
    fprintf (fptr,"initial state = %lu\n", BCG_OT_INITIAL_STATE (bcg_graph));
    fprintf (fptr,"nb states = %lu\n", BCG_OT_NB_STATES (bcg_graph));
    fprintf (fptr,"nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph));
    fprintf (fptr,"nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
    */
-   
-   bcg_nb_states = BCG_OT_NB_STATES (bcg_graph);
-   int last = -1;
-   for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
-      /*fprintf (fptr,"successors of state %lu:\n", bcg_s1);*/
-      
-      BCG_OT_ITERATE_P_LN (bcg_graph, bcg_s1, bcg_label_number, bcg_s2)
-	{
-          fprintf (fptr,"%lu ", bcg_s2);
-      } BCG_OT_END_ITERATE;
-      fprintf (fptr,"%d\n",last);
-   }
-   BCG_OT_READ_BCG_END (&bcg_graph);
-   fclose(fptr);
-   exit (0);
+
+    bcg_nb_states = BCG_OT_NB_STATES(bcg_graph);
+    int last = -1;
+    for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
+        /*fprintf (fptr,"successors of state %lu:\n", bcg_s1);*/
+
+        BCG_OT_ITERATE_P_LN(bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
+            fprintf(fptr, "%lu ", bcg_s2);
+        }
+        BCG_OT_END_ITERATE;
+        fprintf(fptr, "%d\n", last);
+    }
+    BCG_OT_READ_BCG_END(&bcg_graph);
+    fclose(fptr);
+    exit(0);
 }

bcg/src/write_from_file.c

 #include "bcg_user.h"
-int main ( int argc, char* argv[] )
-{
-   BCG_TYPE_STATE_NUMBER S1;
-   BCG_TYPE_LABEL_STRING L = "";
-   BCG_TYPE_STATE_NUMBER S2;
-   BCG_INIT ();
-   char *file_name_give = argv[1];
-   BCG_IO_WRITE_BCG_BEGIN ( file_name_give , 6, 2, "created by tool", 1);
-
-   char *file_name_open = argv[2];
-
-FILE *fptr;
-
-fptr =fopen(file_name_open,"r");
-
-int n;
-
-    fscanf(fptr,"%d", &n);
-
-    for(int i=0;i<n;i++){
-    int num;
-    fscanf(fptr,"%d", &num);
-    S1 = i;
-    while(num!=-1){
-        S2 = num;
-        BCG_IO_WRITE_BCG_EDGE (S1, L , S2);
-        printf("%d %d \n", i, num);
-        fscanf(fptr,"%d", &num);
-    }
+int main(int argc, char *argv[]) {
+    BCG_TYPE_STATE_NUMBER S1;
+    BCG_TYPE_LABEL_STRING L = "";
+    BCG_TYPE_STATE_NUMBER S2;
+    BCG_INIT();
+    char *file_name_give = argv[1];
+    BCG_IO_WRITE_BCG_BEGIN(file_name_give, 6, 2, "created by tool", 1);
+
+    char *file_name_open = argv[2];
+
+    FILE *fptr;
+
+    fptr = fopen(file_name_open, "r");
+
+    int n;
+
+    fscanf(fptr, "%d", &n);
+
+    for (int i = 0; i < n; i++) {
+        int num;
+        fscanf(fptr, "%d", &num);
+        S1 = i;
+        while (num != -1) {
+            S2 = num;
+            BCG_IO_WRITE_BCG_EDGE(S1, L, S2);
+            printf("%d %d \n", i, num);
+            fscanf(fptr, "%d", &num);
+        }
     }
 
-   fclose(fptr);
-   BCG_IO_WRITE_BCG_END ();
+    fclose(fptr);
+    BCG_IO_WRITE_BCG_END();
 
-   return 0;
+    return 0;
 }
-

env.sh

+# Begin Variables to change:
+export FAIRSYN_ROOT="."
+export SYLVAN_PATH="../../libraries/"
+export HOAF_LIB_PATH="/home/tbanerjee/library/cpphoafparser-0.99.2/include"
+# End  Variables to change
+
+# Helpful variables which were created using the above variables:
+
+#
+# fairsyn
+#
+export FAIRSYN_INC=" -I$FAIRSYN_ROOT -I$FAIRSYN_ROOT/utils -I$FAIRSYN_ROOT/lib"
+export FAIRSYN_SRC="$FAIRSYN_ROOT/src"
+export FAIRSYN_BIN="$FAIRSYN_ROOT/bin"
+
+#
+# sylvan
+#
+export SYLVAN_INC=" -I$SYLVAN_PATH/include/ "
+export SYLVAN_LIB=" -L$SYLVAN_PATH/lib -lsylvan "
+
+#
+# hoaf library
+#
+#HOAF_INC		= -isystem $HOAF_LIB_PATH/ast -isystem $HOAF_LIB_PATH/consumer -isystem $HOAF_LIB_PATH/parser
+export HOAF_INC=" -isystem $HOAF_LIB_PATH"
+
+#
+# others
+#
+export MKDIR_P=" mkdir -p "
+export LD_FLAGS=" -ldl "

lib/RabinAutomaton.hh

@@ -6,9 +6,9 @@
 #ifndef RABINAUTOMATON_HH_
 #define RABINAUTOMATON_HH_
 
-#include <stdlib.h>
-#include <math.h>
 #include <fstream>
+#include <math.h>
+#include <stdlib.h>
 
 #include <sylvan_obj.hpp>
 
@@ -22,145 +22,146 @@
  */
 namespace fairsyn {
 
-/* structure containing a single rabin pair */
-struct rabin_pair_ {
-    size_t rabin_index_; /* each rabin pair gets a unique index */
-    sylvan::Bdd G_; /* the states which are to be visited infinitely often */
-    sylvan::Bdd nR_; /* the complement of the states which are to be visited finitely often */
-};
+    /* structure containing a single rabin pair */
+    struct rabin_pair_ {
+        size_t rabin_index_; /* each rabin pair gets a unique index */
+        sylvan::Bdd G_;      /* the states which are to be visited infinitely often */
+        sylvan::Bdd nR_;     /* the complement of the states which are to be visited finitely often */
+    };
 
-class RabinAutomaton {
-public:
-    /* var: stateSpace_ */
-    sylvan::Bdd stateSpace_;
-    /* var: preVars_
+    class RabinAutomaton {
+    public:
+        /* var: stateSpace_ */
+        sylvan::Bdd stateSpace_;
+        /* var: preVars_
      * stores the "pre" state variable indices */
-    std::vector<uint32_t> stateVars_;
-    /* var: inputSpace_ */
-    sylvan::Bdd inputSpace_;
-    /* var: stateSpacePost_ */
-    sylvan::Bdd stateSpacePost_;
-    /* var: postVars_
+        std::vector<uint32_t> stateVars_;
+        /* var: inputSpace_ */
+        sylvan::Bdd inputSpace_;
+        /* var: stateSpacePost_ */
+        sylvan::Bdd stateSpacePost_;
+        /* var: postVars_
      * stores the "post" state variable indices */
-    std::vector<uint32_t> postStateVars_;
-    /* var: transitions_
+        std::vector<uint32_t> postStateVars_;
+        /* var: transitions_
      *  the bdd representing the transition relation as sets of tuples (s,x',s'), where s is pre-state of the rabin automaton, x' is post-state of the symbolic model, and s' is the post-state of the rabin automaton */
-    sylvan::Bdd transitions_;
-    /* var: numRabinPairs_
+        sylvan::Bdd transitions_;
+        /* var: numRabinPairs_
      *  the number of rabin pairs */
-    size_t numRabinPairs_;
-    /* var: RabinPairs_
+        size_t numRabinPairs_;
+        /* var: RabinPairs_
      *  BDD vector[numRabinPairs_][2] containing the rabin pairs {(G_i,~R_i)}, where the Rabin condition is given as:
         \/_i ([]<>G_i & <>[]~R_i)
      * and each G_i,~R_i are given a bdd representing a set of states of the automaton */
-    std::vector<rabin_pair_> RabinPairs_;
-    friend class FixedPoint;
-public:
-    /* constructor: RabinAutomaton
+        std::vector<rabin_pair_> RabinPairs_;
+        friend class FixedPoint;
+
+    public:
+        /* constructor: RabinAutomaton
      * constructs the bdd representation of the Rabin automaton from a given list representation of the states and the transitions
      *
     */
-    RabinAutomaton(std::set<uint32_t>& all_variables,
-                   const sylvan::Bdd& inputSpace,
-                   std::map<std::string, sylvan::Bdd> input_pred_to_bdd,
-                   const std::string filename) {
-        std::ifstream file(filename);
-        cpphoafparser::HOAConsumer::ptr consumer;
-        cpphoafparser::rabin_data data;
-        consumer.reset(new cpphoafparser::HOAConsumerBuildRabin(&data));
-        cpphoafparser::HOAParser::parse(file, consumer);
-        std::map<std::string, sylvan::Bdd> input_id_to_bdd;
-        for (auto it=data.ap_id_map.begin(); it!=data.ap_id_map.end(); ++it) {
-            size_t key=it->first;
-            input_id_to_bdd.insert({std::to_string(key), input_pred_to_bdd[data.ap_id_map[key]]});
-        }
-        /* create a BDD representation of the state space of the rabin automaton */
-        std::vector<uint32_t> state_ids;
-        for (size_t i=0; i<data.States; i++) {
-            state_ids.push_back(uint32_t(i));
-        }
-        uint32_t nvars = (uint32_t)std::ceil(std::log2(data.States));
-        uint32_t max_var_id = *(all_variables.rbegin());
-        /* the "pre" bdd variables */
-        for (uint32_t i=1; i<=nvars; i++) {
-            uint32_t new_var_id = max_var_id+i;
-            stateVars_.push_back(new_var_id);
-            all_variables.insert(new_var_id);
-        }
-        /* the "post" bdd variables */
-        for (uint32_t i=1; i<=nvars; i++) {
-            uint32_t new_var_id = max_var_id+stateVars_.size()+i;
-            postStateVars_.push_back(new_var_id);
-            all_variables.insert(new_var_id);
-        }
-        /* the bdd representing the set of states
+        RabinAutomaton(std::set<uint32_t> &all_variables,
+                       const sylvan::Bdd &inputSpace,
+                       std::map<std::string, sylvan::Bdd> input_pred_to_bdd,
+                       const std::string filename) {
+            std::ifstream file(filename);
+            cpphoafparser::HOAConsumer::ptr consumer;
+            cpphoafparser::rabin_data data;
+            consumer.reset(new cpphoafparser::HOAConsumerBuildRabin(&data));
+            cpphoafparser::HOAParser::parse(file, consumer);
+            std::map<std::string, sylvan::Bdd> input_id_to_bdd;
+            for (auto it = data.ap_id_map.begin(); it != data.ap_id_map.end(); ++it) {
+                size_t key = it->first;
+                input_id_to_bdd.insert({std::to_string(key), input_pred_to_bdd[data.ap_id_map[key]]});
+            }
+            /* create a BDD representation of the state space of the rabin automaton */
+            std::vector<uint32_t> state_ids;
+            for (size_t i = 0; i < data.States; i++) {
+                state_ids.push_back(uint32_t(i));
+            }
+            uint32_t nvars = (uint32_t)std::ceil(std::log2(data.States));
+            uint32_t max_var_id = *(all_variables.rbegin());
+            /* the "pre" bdd variables */
+            for (uint32_t i = 1; i <= nvars; i++) {
+                uint32_t new_var_id = max_var_id + i;
+                stateVars_.push_back(new_var_id);
+                all_variables.insert(new_var_id);
+            }
+            /* the "post" bdd variables */
+            for (uint32_t i = 1; i <= nvars; i++) {
+                uint32_t new_var_id = max_var_id + stateVars_.size() + i;
+                postStateVars_.push_back(new_var_id);
+                all_variables.insert(new_var_id);
+            }
+            /* the bdd representing the set of states
          * given in terms of the "pre" variables */
-        sylvan::BddSet stateBddVars=sylvan::BddSet::fromVector(stateVars_);
-        stateSpace_=helper::SetToBdd(state_ids, stateBddVars, nvars);
-        sylvan::BddSet postStateBddVars=sylvan::BddSet::fromVector(postStateVars_);
-        stateSpacePost_=helper::SetToBdd(state_ids, postStateBddVars, nvars);
-        inputSpace_=inputSpace;
-        /* build the transitions bdd */
-        transitions_=sylvan::Bdd::bddZero();
-        for (size_t i=0; i<data.Transitions.size(); i++) {
-            sylvan::Bdd cube=sylvan::Bdd::bddOne();
-            size_t v=data.Transitions[i].state_id;
-            cube &= helper::ElementToBdd(v, stateBddVars, nvars);
-            std::stack<cpphoafparser::HOAConsumer::label_expr::ptr> nodes;
-            nodes.push(data.Transitions[i].label);
-            while (nodes.size()!=0) {
-                cpphoafparser::HOAConsumer::label_expr::ptr curr_node = nodes.top();
-                nodes.pop();
-                if (curr_node->isAND()) {
-                    nodes.push(curr_node->getLeft());
-                    nodes.push(curr_node->getRight());
-                } else if (curr_node->isNOT()) {
-                    cube &= !(input_id_to_bdd[curr_node->getLeft()->toString()]);
-                } else if (curr_node->isAtom()) {
-                    cube &= input_id_to_bdd[curr_node->toString()];
+            sylvan::BddSet stateBddVars = sylvan::BddSet::fromVector(stateVars_);
+            stateSpace_ = helper::SetToBdd(state_ids, stateBddVars, nvars);
+            sylvan::BddSet postStateBddVars = sylvan::BddSet::fromVector(postStateVars_);
+            stateSpacePost_ = helper::SetToBdd(state_ids, postStateBddVars, nvars);
+            inputSpace_ = inputSpace;
+            /* build the transitions bdd */
+            transitions_ = sylvan::Bdd::bddZero();
+            for (size_t i = 0; i < data.Transitions.size(); i++) {
+                sylvan::Bdd cube = sylvan::Bdd::bddOne();
+                size_t v = data.Transitions[i].state_id;
+                cube &= helper::ElementToBdd(v, stateBddVars, nvars);
+                std::stack<cpphoafparser::HOAConsumer::label_expr::ptr> nodes;
+                nodes.push(data.Transitions[i].label);
+                while (nodes.size() != 0) {
+                    cpphoafparser::HOAConsumer::label_expr::ptr curr_node = nodes.top();
+                    nodes.pop();
+                    if (curr_node->isAND()) {
+                        nodes.push(curr_node->getLeft());
+                        nodes.push(curr_node->getRight());
+                    } else if (curr_node->isNOT()) {
+                        cube &= !(input_id_to_bdd[curr_node->getLeft()->toString()]);
+                    } else if (curr_node->isAtom()) {
+                        cube &= input_id_to_bdd[curr_node->toString()];
+                    }
                 }
+                v = data.Transitions[i].post_id;
+                cube &= helper::ElementToBdd(v, postStateBddVars, nvars);
+                transitions_ |= cube;
             }
-            v=data.Transitions[i].post_id;
-            cube &= helper::ElementToBdd(v, postStateBddVars, nvars);
-            transitions_ |= cube;
-        }
-        /* build the rabin pairs in terms of the pre variables */
-        numRabinPairs_=data.acc_pairs.size();
-        for (size_t i=0; i<numRabinPairs_; i++) {
-            rabin_pair_ pair;
-            pair.rabin_index_=i;
-            /* first, create the BDD for the G sets */
-            std::vector<size_t> v={data.acc_signature[data.acc_pairs[i][0]]};
-            pair.G_=sylvan::Bdd::bddZero();
-            for (size_t j=0; j<v.size(); j++) {
-                size_t temp=v[j];
-                pair.G_ |= helper::ElementToBdd(temp, stateBddVars, nvars);
-            }
-            /* second, create the BDD for the COMPLEMENT OF the R sets */
-            v={data.acc_signature[data.acc_pairs[i][1]]};
-            sylvan::Bdd R=sylvan::Bdd::bddZero();
-            for (size_t j=0; j<v.size(); j++) {
-                size_t temp=v[j];
-                R |= helper::ElementToBdd(temp, stateBddVars, nvars);
+            /* build the rabin pairs in terms of the pre variables */
+            numRabinPairs_ = data.acc_pairs.size();
+            for (size_t i = 0; i < numRabinPairs_; i++) {
+                rabin_pair_ pair;
+                pair.rabin_index_ = i;
+                /* first, create the BDD for the G sets */
+                std::vector<size_t> v = {data.acc_signature[data.acc_pairs[i][0]]};
+                pair.G_ = sylvan::Bdd::bddZero();
+                for (size_t j = 0; j < v.size(); j++) {
+                    size_t temp = v[j];
+                    pair.G_ |= helper::ElementToBdd(temp, stateBddVars, nvars);
+                }
+                /* second, create the BDD for the COMPLEMENT OF the R sets */
+                v = {data.acc_signature[data.acc_pairs[i][1]]};
+                sylvan::Bdd R = sylvan::Bdd::bddZero();
+                for (size_t j = 0; j < v.size(); j++) {
+                    size_t temp = v[j];
+                    R |= helper::ElementToBdd(temp, stateBddVars, nvars);
+                }
+                pair.nR_ = (!R) & stateSpace_;
+                //            for (size_t j=static_cast<size_t>(stateSpace_->getFirstGridPoint()[0]); j<=static_cast<size_t>(stateSpace_->getLastGridPoint()[0]); j++) {
+                //                bool isInR=false;
+                //                for (size_t k=0; k<v.size(); k++) {
+                //                    if (v[k] == j) {
+                //                        isInR=true;
+                //                        break;
+                //                    }
+                //                }
+                //                if (!isInR) {
+                //                    std::vector<size_t> temp={j};
+                //                    pair.nR_ |= stateSpace_->elementToMinterm(temp);
+                //                }
+                //            }
+                RabinPairs_.push_back(pair);
             }
-            pair.nR_= (!R) & stateSpace_;
-//            for (size_t j=static_cast<size_t>(stateSpace_->getFirstGridPoint()[0]); j<=static_cast<size_t>(stateSpace_->getLastGridPoint()[0]); j++) {
-//                bool isInR=false;
-//                for (size_t k=0; k<v.size(); k++) {
-//                    if (v[k] == j) {
-//                        isInR=true;
-//                        break;
-//                    }
-//                }
-//                if (!isInR) {
-//                    std::vector<size_t> temp={j};
-//                    pair.nR_ |= stateSpace_->elementToMinterm(temp);
-//                }
-//            }
-            RabinPairs_.push_back(pair);
         }
-    }
-}; /* close class def */
-} /* close namespace */
+    }; /* close class def */
+}// namespace fairsyn
 
 #endif /* RABINAUTOMATON_HH_ */

lib/fairsyn.hh

 #include "lib/Arena.hh"
 #include "lib/FixedPoint.hh"
 #include "lib/RabinAutomaton.hh"
-#include "utils/testlib.h"
 #include "utils/TicToc.hh"
-
+#include "utils/testlib.h"