Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • kmallik/fairsyn
1 result
Show changes
Commits on Source (6)
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 5961 additions and 5239 deletions
.clang-format 0 → 100644
View file @ b88160a8
---
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
View file @ b88160a8
...@@ -4,84 +4,43 @@ ...@@ -4,84 +4,43 @@
CC = g++ CC = g++
#CC = g++-10 #CC = g++-10
#CXXFLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors #CXX_FLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors
CXXFLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors -g CXX_FLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors -g
#CXXFLAGS = -Wall -Wextra -std=c++11 -O3 #CXX_FLAGS = -Wall -Wextra -std=c++11 -O3
#CXXFLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors -O1 #CXX_FLAGS = -Wall -Wextra -std=c++11 -Wfatal-errors -O1
#
# linker flags
# #
#LDFLAGS = -ldl -lomp # Targets
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
# #
# 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 # object files
# #
OBJF = $(TARGETF).o OBJF = $(TARGET_F).o
OBJS = $(TARGETS).o OBJS = $(TARGET_S).o
.PHONY: directories .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): $(FAIRSYN_BIN):
$(MKDIR_P) $(FAIRSYNBIN) $(MKDIR_P) $(FAIRSYN_BIN)
$(FAIRSYNBIN)/%.o:$(FAIRSYNSRC)/%.cc $(FAIRSYN_BIN)/%.o:$(FAIRSYN_SRC)/%.cc
$(CC) -c -o $@ $< $(CXXFLAGS) $(HOAFINC) $(SYLVANINC) $(FAIRSYNINC) $(CC) -c -o $@ $< $(CXX_FLAGS) $(HOAF_INC) $(SYLVAN_INC) $(FAIRSYN_INC)
$(TARGETF): $(OBJF) $(TARGET_F): $(OBJF)
$(CC) $(CXXFLAGS) -o $@ $^ $(LDFLAGS) $(SYLVANLIB) $(CC) $(CXX_FLAGS) -o $@ $^ $(LD_FLAGS) $(SYLVAN_LIB)
$(TARGETS): $(OBJS) $(TARGET_S): $(OBJS)
$(CC) $(CXXFLAGS) -o $@ $^ $(LDFLAGS) $(SYLVANLIB) $(CC) $(CXX_FLAGS) -o $@ $^ $(LD_FLAGS) $(SYLVAN_LIB)
clean: clean:
rm $(TARGETS) $(TARGETS).o $(TARGETF) $(TARGETF).o rm $(TARGET_S) $(TARGET_S).o $(TARGET_F) $(TARGET_F).o
README.md
View file @ b88160a8
# synthesis-with-edge-fairness # synthesis-with-edge-fairness
Parallel reactive synthesis for omega-regular specifications under the transition fairness condition Parallel reactive synthesis for omega-regular specifications under the transition fairness condition
\ No newline at end of file
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
View file @ b88160a8
#include <iostream>
#include <fstream> #include <fstream>
#include <iostream>
#include <string> #include <string>
using namespace std; using namespace std;
int main(){ int main() {
fstream newfile; fstream newfile;
//cout<<"hi\n"; //cout<<"hi\n";
newfile.open("cwi_1_2.txt",ios::in); newfile.open("cwi_1_2.txt", ios::in);
int n; int n;
newfile>>n; newfile >> n;
cout<<n<<"\n"; cout << n << "\n";
while(n--){ while (n--) {
int num; int num;
newfile>>num; newfile >> num;
while(num!=-1){ while (num != -1) {
cout<<num<<" "; cout << num << " ";
newfile>>num; newfile >> num;
} }
cout<<"\n"; cout << "\n";
} }
newfile.close(); newfile.close();
return 0; return 0;
} }
bcg/other_codes/Experiment.c
View file @ b88160a8
#include "bcg_user.h" #include "bcg_user.h"
/* The following function prints information about a BCG graph */ /* The following function prints information about a BCG graph */
void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph) void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
{ printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(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 states = %lu\n", BCG_OT_NB_STATES (bcg_graph)); printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph)); printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
} }
/* The following function displays an edge */ /* 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 ) 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_C_STRING bcg_label_string;
BCG_TYPE_BOOLEAN bcg_visible; BCG_TYPE_BOOLEAN bcg_visible;
BCG_TYPE_NATURAL bcg_cardinal; BCG_TYPE_NATURAL bcg_cardinal;
BCG_TYPE_C_STRING bcg_gate; BCG_TYPE_C_STRING bcg_gate;
bcg_label_string = BCG_OT_LABEL_STRING (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_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
bcg_cardinal = BCG_OT_LABEL_CARDINAL (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); bcg_state_1, bcg_state_2);
printf ("label unique number = %u\n", bcg_label_number); printf("label unique number = %u\n", bcg_label_number);
printf ("label string = %s\n", bcg_label_string); printf("label string = %s\n", bcg_label_string);
printf ("label cardinal = %u\n", bcg_cardinal); printf("label cardinal = %u\n", bcg_cardinal);
if (bcg_visible) { if (bcg_visible) {
bcg_gate = BCG_OT_LABEL_GATE (bcg_graph, bcg_label_number); bcg_gate = BCG_OT_LABEL_GATE(bcg_graph, bcg_label_number);
printf ("visible label (gate = %s)\n", bcg_gate); printf("visible label (gate = %s)\n", bcg_gate);
} else { } else {
bcg_gate = BCG_OT_LABEL_HIDDEN_GATE (bcg_graph, bcg_label_number); bcg_gate = BCG_OT_LABEL_HIDDEN_GATE(bcg_graph, bcg_label_number);
printf ("hidden label (hidden gate = %s)\n", bcg_gate); printf("hidden label (hidden gate = %s)\n", bcg_gate);
} }
} }
int main () int main() {
{ BCG_TYPE_OBJECT_TRANSITION bcg_graph;
BCG_TYPE_OBJECT_TRANSITION bcg_graph; BCG_TYPE_STATE_NUMBER bcg_s1;
BCG_TYPE_STATE_NUMBER bcg_s1; BCG_TYPE_LABEL_NUMBER bcg_label_number;
BCG_TYPE_LABEL_NUMBER bcg_label_number; BCG_TYPE_STATE_NUMBER bcg_s2;
BCG_TYPE_STATE_NUMBER bcg_s2; BCG_TYPE_STATE_NUMBER bcg_nb_states;
BCG_TYPE_STATE_NUMBER bcg_nb_states; BCG_TYPE_C_STRING bcg_label_string;
BCG_TYPE_C_STRING bcg_label_string;
BCG_INIT (); BCG_INIT();
BCG_OT_READ_BCG_BEGIN ("vasy_0_1.bcg", &bcg_graph, 0); BCG_OT_READ_BCG_BEGIN("vasy_0_1.bcg", &bcg_graph, 0);
bcg_print_info (bcg_graph); 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);
}
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); BCG_OT_READ_BCG_END(&bcg_graph);
exit (0); exit(0);
} }
bcg/other_codes/Read.c
View file @ b88160a8
#include "bcg_user.h" #include "bcg_user.h"
/* The following function prints information about a BCG graph */ /* The following function prints information about a BCG graph */
void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph) void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
{ printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(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 states = %lu\n", BCG_OT_NB_STATES (bcg_graph)); printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph)); printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
} }
/* The following function displays an edge */ /* 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 ) 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_C_STRING bcg_label_string; BCG_TYPE_BOOLEAN bcg_visible;
BCG_TYPE_BOOLEAN bcg_visible; BCG_TYPE_NATURAL bcg_cardinal;
BCG_TYPE_NATURAL bcg_cardinal; BCG_TYPE_C_STRING bcg_gate;
BCG_TYPE_C_STRING bcg_gate;
bcg_label_string = BCG_OT_LABEL_STRING (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_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
bcg_cardinal = BCG_OT_LABEL_CARDINAL (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); bcg_state_1, bcg_state_2);
printf ("label unique number = %u\n", bcg_label_number); printf("label unique number = %u\n", bcg_label_number);
printf ("label string = %s\n", bcg_label_string); printf("label string = %s\n", bcg_label_string);
printf ("label cardinal = %u\n", bcg_cardinal); printf("label cardinal = %u\n", bcg_cardinal);
if (bcg_visible) { if (bcg_visible) {
bcg_gate = BCG_OT_LABEL_GATE (bcg_graph, bcg_label_number); bcg_gate = BCG_OT_LABEL_GATE(bcg_graph, bcg_label_number);
printf ("visible label (gate = %s)\n", bcg_gate); printf("visible label (gate = %s)\n", bcg_gate);
} else { } else {
bcg_gate = BCG_OT_LABEL_HIDDEN_GATE (bcg_graph, bcg_label_number); bcg_gate = BCG_OT_LABEL_HIDDEN_GATE(bcg_graph, bcg_label_number);
printf ("hidden label (hidden gate = %s)\n", bcg_gate); printf("hidden label (hidden gate = %s)\n", bcg_gate);
} }
} }
int main () int main() {
{ BCG_TYPE_OBJECT_TRANSITION bcg_graph;
BCG_TYPE_OBJECT_TRANSITION bcg_graph; BCG_TYPE_STATE_NUMBER bcg_s1;
BCG_TYPE_STATE_NUMBER bcg_s1; BCG_TYPE_LABEL_NUMBER bcg_label_number;
BCG_TYPE_LABEL_NUMBER bcg_label_number; BCG_TYPE_STATE_NUMBER bcg_s2;
BCG_TYPE_STATE_NUMBER bcg_s2; BCG_TYPE_STATE_NUMBER bcg_nb_states;
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_OT_READ_BCG_END(&bcg_graph);
bcg_print_info (bcg_graph); BCG_OT_READ_BCG_BEGIN("vasy_0_1.bcg", &bcg_graph, 1);
BCG_OT_ITERATE_PLN (bcg_graph, bcg_s1, bcg_label_number, bcg_s2) { bcg_print_info(bcg_graph);
bcg_print_edge (bcg_graph, bcg_s1, bcg_label_number, bcg_s2); bcg_nb_states = BCG_OT_NB_STATES(bcg_graph);
} BCG_OT_END_ITERATE; for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
printf("successors of state %lu:\n", bcg_s1);
BCG_OT_READ_BCG_END (&bcg_graph); BCG_OT_ITERATE_P_LN(bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
BCG_OT_READ_BCG_BEGIN ("vasy_0_1.bcg", &bcg_graph, 1); bcg_print_edge(bcg_graph, bcg_s1, bcg_label_number, bcg_s2);
bcg_print_info (bcg_graph); }
bcg_nb_states = BCG_OT_NB_STATES (bcg_graph); BCG_OT_END_ITERATE;
for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) { }
printf ("successors of state %lu:\n", bcg_s1); BCG_OT_READ_BCG_END(&bcg_graph);
BCG_OT_ITERATE_P_LN (bcg_graph, bcg_s1, bcg_label_number, bcg_s2) exit(0);
{
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
View file @ b88160a8
#include "bcg_user.h" #include "bcg_user.h"
int main () int main() {
{ BCG_TYPE_STATE_NUMBER S1;
BCG_TYPE_STATE_NUMBER S1; BCG_TYPE_LABEL_STRING L = "";
BCG_TYPE_LABEL_STRING L = ""; BCG_TYPE_STATE_NUMBER S2;
BCG_TYPE_STATE_NUMBER S2; BCG_INIT();
BCG_INIT (); BCG_IO_WRITE_BCG_BEGIN("test.bcg", 0, 2, "created by tool", 1);
BCG_IO_WRITE_BCG_BEGIN ("test.bcg", 0, 2, "created by tool", 1); for (int i = 0; i < 10; i++) {
for(int i=0;i<10;i++) S1 = i;
{ for (int j = i + 1; j < 10; j++) {
S1 = i; S2 = j;
for(int j=i+1;j<10;j++){ BCG_IO_WRITE_BCG_EDGE(S1, L, S2);
S2 = j; }
BCG_IO_WRITE_BCG_EDGE (S1, L , S2); }
} BCG_IO_WRITE_BCG_END();
} return (0);
BCG_IO_WRITE_BCG_END ();
return (0);
} }
bcg/src/Extraction.c
View file @ b88160a8
#include "bcg_user.h" #include "bcg_user.h"
/* The following function prints information about a BCG graph */ /* The following function prints information about a BCG graph */
void bcg_print_info (BCG_TYPE_OBJECT_TRANSITION bcg_graph) void bcg_print_info(BCG_TYPE_OBJECT_TRANSITION bcg_graph) {
{ printf("initial state = %lu\n", BCG_OT_INITIAL_STATE(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 states = %lu\n", BCG_OT_NB_STATES (bcg_graph)); printf("nb edges = %lu\n", BCG_OT_NB_EDGES(bcg_graph));
printf ("nb edges = %lu\n", BCG_OT_NB_EDGES (bcg_graph)); printf("nb labels = %u\n", BCG_OT_NB_LABELS(bcg_graph));
printf ("nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
} }
/* The following function displays an edge */ /* 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 ) 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_C_STRING bcg_label_string; BCG_TYPE_BOOLEAN bcg_visible;
BCG_TYPE_BOOLEAN bcg_visible; BCG_TYPE_NATURAL bcg_cardinal;
BCG_TYPE_NATURAL bcg_cardinal; BCG_TYPE_C_STRING bcg_gate;
BCG_TYPE_C_STRING bcg_gate;
bcg_label_string = BCG_OT_LABEL_STRING (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_visible = BCG_OT_LABEL_VISIBLE(bcg_graph, bcg_label_number);
bcg_cardinal = BCG_OT_LABEL_CARDINAL (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", fprintf("transition from state %lu to state %lu\n",
bcg_state_1, bcg_state_2); bcg_state_1, bcg_state_2);
/*printf ("label unique number = %u\n", bcg_label_number); /*printf ("label unique number = %u\n", bcg_label_number);
printf ("label string = %s\n", bcg_label_string); printf ("label string = %s\n", bcg_label_string);
printf ("label cardinal = %u\n", bcg_cardinal); printf ("label cardinal = %u\n", bcg_cardinal);
if (bcg_visible) { if (bcg_visible) {
...@@ -37,61 +35,60 @@ void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBE ...@@ -37,61 +35,60 @@ void bcg_print_edge (BCG_TYPE_OBJECT_TRANSITION bcg_graph , BCG_TYPE_STATE_NUMBE
} }
int main (int argc, char *argv[]) int main(int argc, char *argv[]) {
{ FILE *fptr;
FILE *fptr; char *file_path1 = "../output/";
char * file_path1 = "../output/"; char *file_path2 = "../input/";
char * file_path2 = "../input/"; char *file_extention1 = ".txt";
char * file_extention1 = ".txt"; char *file_extention2 = ".bcg";
char * file_extention2 = ".bcg";
int size_fileopen = strlen(argv[1]) + strlen(file_path1) + strlen(file_extention1) + 1; int size_fileopen = strlen(argv[1]) + strlen(file_path1) + strlen(file_extention1) + 1;
char * fileopen = (char *)malloc(size_fileopen); char *fileopen = (char *)malloc(size_fileopen);
strcpy(fileopen , file_path1); strcpy(fileopen, file_path1);
strcat(fileopen , argv[1]); strcat(fileopen, argv[1]);
strcat(fileopen , file_extention1); strcat(fileopen, file_extention1);
fptr =fopen(fileopen,"w"); fptr = fopen(fileopen, "w");
BCG_TYPE_OBJECT_TRANSITION bcg_graph; BCG_TYPE_OBJECT_TRANSITION bcg_graph;
BCG_TYPE_STATE_NUMBER bcg_s1; BCG_TYPE_STATE_NUMBER bcg_s1;
BCG_TYPE_LABEL_NUMBER bcg_label_number; BCG_TYPE_LABEL_NUMBER bcg_label_number;
BCG_TYPE_STATE_NUMBER bcg_s2; BCG_TYPE_STATE_NUMBER bcg_s2;
BCG_TYPE_STATE_NUMBER bcg_nb_states; BCG_TYPE_STATE_NUMBER bcg_nb_states;
int size_bcgopen = strlen(argv[1]) + strlen(file_path2) + strlen(file_extention2) + 1; int size_bcgopen = strlen(argv[1]) + strlen(file_path2) + strlen(file_extention2) + 1;
char * bcgopen = (char *)malloc(size_bcgopen); char *bcgopen = (char *)malloc(size_bcgopen);
strcpy(bcgopen , file_path2); strcpy(bcgopen, file_path2);
strcat(bcgopen , argv[1]); strcat(bcgopen, argv[1]);
strcat(bcgopen , file_extention2); strcat(bcgopen, file_extention2);
BCG_INIT (); BCG_INIT();
BCG_OT_READ_BCG_BEGIN (bcgopen, &bcg_graph, 1); BCG_OT_READ_BCG_BEGIN(bcgopen, &bcg_graph, 1);
int initial_state = BCG_OT_INITIAL_STATE (bcg_graph); int initial_state = BCG_OT_INITIAL_STATE(bcg_graph);
int number_of_states = BCG_OT_NB_STATES (bcg_graph); int number_of_states = BCG_OT_NB_STATES(bcg_graph);
int number_of_edges = BCG_OT_NB_EDGES (bcg_graph); int number_of_edges = BCG_OT_NB_EDGES(bcg_graph);
fprintf(fptr,"%lu\n",number_of_states); fprintf(fptr, "%lu\n", number_of_states);
/* /*
fprintf (fptr,"initial state = %lu\n", BCG_OT_INITIAL_STATE (bcg_graph)); 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 states = %lu\n", BCG_OT_NB_STATES (bcg_graph));
fprintf (fptr,"nb edges = %lu\n", BCG_OT_NB_EDGES (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)); fprintf (fptr,"nb labels = %u\n", BCG_OT_NB_LABELS (bcg_graph));
*/ */
bcg_nb_states = BCG_OT_NB_STATES (bcg_graph); bcg_nb_states = BCG_OT_NB_STATES(bcg_graph);
int last = -1; int last = -1;
for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) { for (bcg_s1 = 0; bcg_s1 < bcg_nb_states; bcg_s1++) {
/*fprintf (fptr,"successors of state %lu:\n", 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) BCG_OT_ITERATE_P_LN(bcg_graph, bcg_s1, bcg_label_number, bcg_s2) {
{ fprintf(fptr, "%lu ", bcg_s2);
fprintf (fptr,"%lu ", bcg_s2); }
} BCG_OT_END_ITERATE; BCG_OT_END_ITERATE;
fprintf (fptr,"%d\n",last); fprintf(fptr, "%d\n", last);
} }
BCG_OT_READ_BCG_END (&bcg_graph); BCG_OT_READ_BCG_END(&bcg_graph);
fclose(fptr); fclose(fptr);
exit (0); exit(0);
} }
bcg/src/write_from_file.c
View file @ b88160a8
#include "bcg_user.h" #include "bcg_user.h"
int main ( int argc, char* argv[] ) int main(int argc, char *argv[]) {
{ BCG_TYPE_STATE_NUMBER S1;
BCG_TYPE_STATE_NUMBER S1; BCG_TYPE_LABEL_STRING L = "";
BCG_TYPE_LABEL_STRING L = ""; BCG_TYPE_STATE_NUMBER S2;
BCG_TYPE_STATE_NUMBER S2; BCG_INIT();
BCG_INIT (); char *file_name_give = argv[1];
char *file_name_give = argv[1]; BCG_IO_WRITE_BCG_BEGIN(file_name_give, 6, 2, "created by tool", 1);
BCG_IO_WRITE_BCG_BEGIN ( file_name_give , 6, 2, "created by tool", 1);
char *file_name_open = argv[2];
char *file_name_open = argv[2];
FILE *fptr;
FILE *fptr;
fptr = fopen(file_name_open, "r");
fptr =fopen(file_name_open,"r");
int n;
int n;
fscanf(fptr, "%d", &n);
fscanf(fptr,"%d", &n);
for (int i = 0; i < n; i++) {
for(int i=0;i<n;i++){ int num;
int num; fscanf(fptr, "%d", &num);
fscanf(fptr,"%d", &num); S1 = i;
S1 = i; while (num != -1) {
while(num!=-1){ S2 = num;
S2 = num; BCG_IO_WRITE_BCG_EDGE(S1, L, S2);
BCG_IO_WRITE_BCG_EDGE (S1, L , S2); printf("%d %d \n", i, num);
printf("%d %d \n", i, num); fscanf(fptr, "%d", &num);
fscanf(fptr,"%d", &num); }
}
} }
fclose(fptr); fclose(fptr);
BCG_IO_WRITE_BCG_END (); BCG_IO_WRITE_BCG_END();
return 0; return 0;
} }
env.sh 0 → 100644
View file @ b88160a8
# 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 "
examples/lego/example.cc
View file @ b88160a8
This diff is collapsed.
examples/lego/fairsyn_example.cc
View file @ b88160a8
This diff is collapsed.
examples/lego/inpout_example.cc
View file @ b88160a8
This diff is collapsed.
examples/lego/lego_fairsyn.cc
View file @ b88160a8
This diff is collapsed.
examples/lego/modified_example.cc
View file @ b88160a8
This diff is collapsed.
lib/Arena.hh
View file @ b88160a8
This diff is collapsed.
lib/FixedPoint.hh
View file @ b88160a8
This diff is collapsed.
lib/OLD_FixedPoint.hh 0 → 100644
View file @ b88160a8
This diff is collapsed.
lib/RabinAutomaton.hh
View file @ b88160a8
...@@ -6,9 +6,9 @@ ...@@ -6,9 +6,9 @@
#ifndef RABINAUTOMATON_HH_ #ifndef RABINAUTOMATON_HH_
#define RABINAUTOMATON_HH_ #define RABINAUTOMATON_HH_
#include <stdlib.h>
#include <math.h>
#include <fstream> #include <fstream>
#include <math.h>
#include <stdlib.h>
#include <sylvan_obj.hpp> #include <sylvan_obj.hpp>
...@@ -22,145 +22,146 @@ ...@@ -22,145 +22,146 @@
*/ */
namespace fairsyn { namespace fairsyn {
/* structure containing a single rabin pair */ /* structure containing a single rabin pair */
struct rabin_pair_ { struct rabin_pair_ {
size_t rabin_index_; /* each rabin pair gets a unique index */ 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 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 */ sylvan::Bdd nR_; /* the complement of the states which are to be visited finitely often */
}; };
class RabinAutomaton { class RabinAutomaton {
public: public:
/* var: stateSpace_ */ /* var: stateSpace_ */
sylvan::Bdd stateSpace_; sylvan::Bdd stateSpace_;
/* var: preVars_ /* var: preVars_
* stores the "pre" state variable indices */ * stores the "pre" state variable indices */
std::vector<uint32_t> stateVars_; std::vector<uint32_t> stateVars_;
/* var: inputSpace_ */ /* var: inputSpace_ */
sylvan::Bdd inputSpace_; sylvan::Bdd inputSpace_;
/* var: stateSpacePost_ */ /* var: stateSpacePost_ */
sylvan::Bdd stateSpacePost_; sylvan::Bdd stateSpacePost_;
/* var: postVars_ /* var: postVars_
* stores the "post" state variable indices */ * stores the "post" state variable indices */
std::vector<uint32_t> postStateVars_; std::vector<uint32_t> postStateVars_;
/* var: transitions_ /* 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 */ * 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_; sylvan::Bdd transitions_;
/* var: numRabinPairs_ /* var: numRabinPairs_
* the number of rabin pairs */ * the number of rabin pairs */
size_t numRabinPairs_; size_t numRabinPairs_;
/* var: RabinPairs_ /* var: RabinPairs_
* BDD vector[numRabinPairs_][2] containing the rabin pairs {(G_i,~R_i)}, where the Rabin condition is given as: * BDD vector[numRabinPairs_][2] containing the rabin pairs {(G_i,~R_i)}, where the Rabin condition is given as:
\/_i ([]<>G_i & <>[]~R_i) \/_i ([]<>G_i & <>[]~R_i)
* and each G_i,~R_i are given a bdd representing a set of states of the automaton */ * and each G_i,~R_i are given a bdd representing a set of states of the automaton */
std::vector<rabin_pair_> RabinPairs_; std::vector<rabin_pair_> RabinPairs_;
friend class FixedPoint; friend class FixedPoint;
public:
/* constructor: RabinAutomaton public:
/* constructor: RabinAutomaton
* constructs the bdd representation of the Rabin automaton from a given list representation of the states and the transitions * 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, RabinAutomaton(std::set<uint32_t> &all_variables,
const sylvan::Bdd& inputSpace, const sylvan::Bdd &inputSpace,
std::map<std::string, sylvan::Bdd> input_pred_to_bdd, std::map<std::string, sylvan::Bdd> input_pred_to_bdd,
const std::string filename) { const std::string filename) {
std::ifstream file(filename); std::ifstream file(filename);
cpphoafparser::HOAConsumer::ptr consumer; cpphoafparser::HOAConsumer::ptr consumer;
cpphoafparser::rabin_data data; cpphoafparser::rabin_data data;
consumer.reset(new cpphoafparser::HOAConsumerBuildRabin(&data)); consumer.reset(new cpphoafparser::HOAConsumerBuildRabin(&data));
cpphoafparser::HOAParser::parse(file, consumer); cpphoafparser::HOAParser::parse(file, consumer);
std::map<std::string, sylvan::Bdd> input_id_to_bdd; 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) { for (auto it = data.ap_id_map.begin(); it != data.ap_id_map.end(); ++it) {
size_t key=it->first; size_t key = it->first;
input_id_to_bdd.insert({std::to_string(key), input_pred_to_bdd[data.ap_id_map[key]]}); 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 */ /* create a BDD representation of the state space of the rabin automaton */
std::vector<uint32_t> state_ids; std::vector<uint32_t> state_ids;
for (size_t i=0; i<data.States; i++) { for (size_t i = 0; i < data.States; i++) {
state_ids.push_back(uint32_t(i)); state_ids.push_back(uint32_t(i));
} }
uint32_t nvars = (uint32_t)std::ceil(std::log2(data.States)); uint32_t nvars = (uint32_t)std::ceil(std::log2(data.States));
uint32_t max_var_id = *(all_variables.rbegin()); uint32_t max_var_id = *(all_variables.rbegin());
/* the "pre" bdd variables */ /* the "pre" bdd variables */
for (uint32_t i=1; i<=nvars; i++) { for (uint32_t i = 1; i <= nvars; i++) {
uint32_t new_var_id = max_var_id+i; uint32_t new_var_id = max_var_id + i;
stateVars_.push_back(new_var_id); stateVars_.push_back(new_var_id);
all_variables.insert(new_var_id); all_variables.insert(new_var_id);
} }
/* the "post" bdd variables */ /* the "post" bdd variables */
for (uint32_t i=1; i<=nvars; i++) { for (uint32_t i = 1; i <= nvars; i++) {
uint32_t new_var_id = max_var_id+stateVars_.size()+i; uint32_t new_var_id = max_var_id + stateVars_.size() + i;
postStateVars_.push_back(new_var_id); postStateVars_.push_back(new_var_id);
all_variables.insert(new_var_id); all_variables.insert(new_var_id);
} }
/* the bdd representing the set of states /* the bdd representing the set of states
* given in terms of the "pre" variables */ * given in terms of the "pre" variables */
sylvan::BddSet stateBddVars=sylvan::BddSet::fromVector(stateVars_); sylvan::BddSet stateBddVars = sylvan::BddSet::fromVector(stateVars_);
stateSpace_=helper::SetToBdd(state_ids, stateBddVars, nvars); stateSpace_ = helper::SetToBdd(state_ids, stateBddVars, nvars);
sylvan::BddSet postStateBddVars=sylvan::BddSet::fromVector(postStateVars_); sylvan::BddSet postStateBddVars = sylvan::BddSet::fromVector(postStateVars_);
stateSpacePost_=helper::SetToBdd(state_ids, postStateBddVars, nvars); stateSpacePost_ = helper::SetToBdd(state_ids, postStateBddVars, nvars);
inputSpace_=inputSpace; inputSpace_ = inputSpace;
/* build the transitions bdd */ /* build the transitions bdd */
transitions_=sylvan::Bdd::bddZero(); transitions_ = sylvan::Bdd::bddZero();
for (size_t i=0; i<data.Transitions.size(); i++) { for (size_t i = 0; i < data.Transitions.size(); i++) {
sylvan::Bdd cube=sylvan::Bdd::bddOne(); sylvan::Bdd cube = sylvan::Bdd::bddOne();
size_t v=data.Transitions[i].state_id; size_t v = data.Transitions[i].state_id;
cube &= helper::ElementToBdd(v, stateBddVars, nvars); cube &= helper::ElementToBdd(v, stateBddVars, nvars);
std::stack<cpphoafparser::HOAConsumer::label_expr::ptr> nodes; std::stack<cpphoafparser::HOAConsumer::label_expr::ptr> nodes;
nodes.push(data.Transitions[i].label); nodes.push(data.Transitions[i].label);
while (nodes.size()!=0) { while (nodes.size() != 0) {
cpphoafparser::HOAConsumer::label_expr::ptr curr_node = nodes.top(); cpphoafparser::HOAConsumer::label_expr::ptr curr_node = nodes.top();
nodes.pop(); nodes.pop();
if (curr_node->isAND()) { if (curr_node->isAND()) {
nodes.push(curr_node->getLeft()); nodes.push(curr_node->getLeft());
nodes.push(curr_node->getRight()); nodes.push(curr_node->getRight());
} else if (curr_node->isNOT()) { } else if (curr_node->isNOT()) {
cube &= !(input_id_to_bdd[curr_node->getLeft()->toString()]); cube &= !(input_id_to_bdd[curr_node->getLeft()->toString()]);
} else if (curr_node->isAtom()) { } else if (curr_node->isAtom()) {
cube &= input_id_to_bdd[curr_node->toString()]; 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; /* build the rabin pairs in terms of the pre variables */
cube &= helper::ElementToBdd(v, postStateBddVars, nvars); numRabinPairs_ = data.acc_pairs.size();
transitions_ |= cube; for (size_t i = 0; i < numRabinPairs_; i++) {
} rabin_pair_ pair;
/* build the rabin pairs in terms of the pre variables */ pair.rabin_index_ = i;
numRabinPairs_=data.acc_pairs.size(); /* first, create the BDD for the G sets */
for (size_t i=0; i<numRabinPairs_; i++) { std::vector<size_t> v = {data.acc_signature[data.acc_pairs[i][0]]};
rabin_pair_ pair; pair.G_ = sylvan::Bdd::bddZero();
pair.rabin_index_=i; for (size_t j = 0; j < v.size(); j++) {
/* first, create the BDD for the G sets */ size_t temp = v[j];
std::vector<size_t> v={data.acc_signature[data.acc_pairs[i][0]]}; pair.G_ |= helper::ElementToBdd(temp, stateBddVars, nvars);
pair.G_=sylvan::Bdd::bddZero(); }
for (size_t j=0; j<v.size(); j++) { /* second, create the BDD for the COMPLEMENT OF the R sets */
size_t temp=v[j]; v = {data.acc_signature[data.acc_pairs[i][1]]};
pair.G_ |= helper::ElementToBdd(temp, stateBddVars, nvars); sylvan::Bdd R = sylvan::Bdd::bddZero();
} for (size_t j = 0; j < v.size(); j++) {
/* second, create the BDD for the COMPLEMENT OF the R sets */ size_t temp = v[j];
v={data.acc_signature[data.acc_pairs[i][1]]}; R |= helper::ElementToBdd(temp, stateBddVars, nvars);
sylvan::Bdd R=sylvan::Bdd::bddZero(); }
for (size_t j=0; j<v.size(); j++) { pair.nR_ = (!R) & stateSpace_;
size_t temp=v[j]; // for (size_t j=static_cast<size_t>(stateSpace_->getFirstGridPoint()[0]); j<=static_cast<size_t>(stateSpace_->getLastGridPoint()[0]); j++) {
R |= helper::ElementToBdd(temp, stateBddVars, nvars); // 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 class def */ }// namespace fairsyn
} /* close namespace */
#endif /* RABINAUTOMATON_HH_ */ #endif /* RABINAUTOMATON_HH_ */
lib/fairsyn.hh
View file @ b88160a8
#include "lib/Arena.hh" #include "lib/Arena.hh"
#include "lib/FixedPoint.hh" #include "lib/FixedPoint.hh"
#include "lib/RabinAutomaton.hh" #include "lib/RabinAutomaton.hh"
#include "utils/testlib.h"
#include "utils/TicToc.hh" #include "utils/TicToc.hh"
#include "utils/testlib.h"