verifit / mata Goto Github PK

A fast and simple automata library

License: MIT License

Shell 0.17% C++ 15.68% Python 1.59% Makefile 0.08% CMake 0.40% Cython 1.65% Jupyter Notebook 0.93% Hack 0.05% Stata 79.45%

mata's People

Contributors

Stargazers

Watchers

Forkers

p4l1ly jurajsic tfiedor michalhorky kocotom adda0 vhavlena notvalord zkfn xkoval18 tmokenc

mata's Issues

Discussion of format of headers

What should we have in headers? Should they be somehow uniform?

Project documentation page does not exist

The page https://verifit.github.io/mata referenced from README.md does not exist.

Add support for epsilon

We agreeed that it would be nice to add to alphabets support for defining epsilon.

When using the python binding for RE->NFA translation on the regular expression ((aa)*)*(b)* I get the following error:
libc++abi: terminating with uncaught exception of type std::out_of_range: 0 or 18446744073709551615 is not a state.

Encapsulate transition relation to isolate class

Maybe making classes for transition relation would be good after all. Lets try to discuss here.

The reason is that we actually will want to modify the data structures,
mainly to make extensions of the library. So far, it seems that we will want to:

include counters
include general registers
have a version that mixes BDDs with automata - has binary alphabet and levels of states.

And we will probably want to be able to fine tune some data structures after all. Maybe not much and often, but it would be good to make it possible.

Assert failure while mintermizing AFA

There is an assert failure while mintermizing this AFA:

@AFA-bits
%Initial qQC0_0 & qQC1_0
%Final !qQC0_39 & !qQC0_5 & !qQC1_12 & !qQC0_20 & !qQC1_22 & !qQC0_10 & !qQC1_36 & !qQC0_40 & !qQC1_2 & !qQC1_31 & !qQC0_47 & !qQC1_5 & !qQC1_28 & !qQC0_35 & !qQC1_43 & !qQC0_9 & !qQC1_51 & !qQC1_48 & !qQC0_2 & !qQC1_15 & !qQC0_27 & !qQC0_7 & !qQC1_10 & !qQC0_22 & !qQC1_24 & !qQC0_52 & !qQC0_16 & !qQC1_9 & !qQC0_13 & !qQC1_38 & !qQC1_21 & !qQC0_18 & !qQC1_33 & !qQC0_45 & !qQC1_7 & !qQC0_37 & !qQC1_41 & !qQC0_30 & !qQC1_46 & !qQC0_29 & !qQC1_52 & !qQC0_1 & !qQC1_16 & !qQC0_24 & !qQC0_14 & !qQC0_49 & !qQC1_26 & !qQC0_50 & !qQC0_11 & !qQC1_23 & !qQC1_35 & !qQC0_43 & !qQC1_1 & !qQC1_4 & !qQC1_29 & !qQC1_30 & !qQC0_46 & !qQC0_32 & !qQC1_44 & !qQC1_19 & !qQC1_50 & !qQC1_49 & !qQC0_3 & !qQC1_14 & !qQC0_26 & !qQC0_4 & !qQC1_13 & !qQC0_21 & !qQC0_38 & !qQC1_8 & !qQC1_25 & !qQC0_53 & !qQC0_17 & !qQC1_3 & !qQC1_37 & !qQC0_41 & !qQC1_6 & !qQC0_19 & !qQC1_32 & !qQC0_44 & !qQC0_34 & !qQC1_42 & !qQC0_8 & !qQC0_28 & !qQC0_31 & !qQC1_47 & !qQC1_11 & !qQC0_23 & !qQC0_6 & !qQC1_27 & !qQC0_51 & !qQC0_15 & !qQC0_48 & !qQC1_20 & !qQC0_12 & !qQC1_39 & !qQC1_0 & !qQC1_34 & !qQC0_42 & !qQC0_36 & !qQC1_40 & !qQC1_18 & !qQC0_33 & !qQC1_45 & !qQC0_25 & !qQC1_53 & !qQC0_0 & !qQC1_17
qQC1_34 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_35
qQC0_42 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_43
qQC0_3 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_4
qQC1_40 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_41
qQC0_36 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_37
qQC1_9 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_10
qQC1_10 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_11
qQC1_4 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_5
qQC0_22 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_23
qQC1_3 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_4
qQC0_25 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_26
qQC1_53 !aF
qQC1_17 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_18
qQC1_38 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_39
qQC1_21 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_22
qQC0_13 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_14
qQC1_33 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_34
qQC0_18 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_19
qQC0_45 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_46
qQC0_4 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_5
qQC1_36 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_37
qQC0_40 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_41
qQC0_1 (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_2) | (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_1)
qQC0_30 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_31
qQC0_29 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_30
qQC1_46 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_47
qQC0_35 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_36
qQC1_43 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_44
qQC1_1 aF | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & (aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0))) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & qQC1_1) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & qQC1_2) | (qQC1_2 & qQC1_1)
qQC0_27 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_28
qQC1_51 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_52
qQC1_48 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_49
qQC1_15 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_16
qQC1_23 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_24
qQC0_11 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_12
qQC1_24 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_25
qQC0_16 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_17
qQC0_52 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_53
qQC0_46 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_47
qQC0_7 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_8
qQC1_30 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_31
qQC1_29 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_30
qQC0_32 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_33
qQC1_44 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_45
qQC1_19 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_20
qQC1_8 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_9
qQC1_41 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_42
qQC0_37 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_38
qQC0_21 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_22
qQC1_13 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_14
qQC0_38 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_39
qQC1_7 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_8
qQC0_24 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_25
qQC1_52 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_53
qQC1_16 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_17
qQC1_2 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_3
qQC0_14 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_15
qQC0_49 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_50
qQC0_50 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_51
qQC0_8 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_9
qQC1_26 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_27
qQC0_19 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_20
qQC0_44 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_45
qQC0_5 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_6
qQC1_32 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_33
qQC0_43 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_44
qQC0_2 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_3
qQC1_35 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_36
qQC0_28 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_29
qQC1_47 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_48
qQC0_31 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_32
qQC1_11 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_12
qQC1_5 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_6
qQC0_23 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_24
qQC1_50 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_51
qQC1_49 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_50
qQC1_14 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_15
qQC1_0 aF | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & (aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0)) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0)) & qQC1_2) | ((aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | !aV0) & qQC1_1) | (qQC1_1 & qQC1_2)
qQC0_26 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_27
qQC0_12 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_13
qQC1_39 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_40
qQC1_20 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_21
qQC0_53 aF
qQC1_25 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_26
qQC0_17 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_18
qQC0_41 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_42
qQC0_0 (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_1) | (!aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & aV0 & qQC0_2)
qQC1_37 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_38
qQC1_45 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_46
qQC1_18 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_19
qQC0_33 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_34
qQC1_42 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_43
qQC0_34 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_35
qQC1_12 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_13
qQC0_39 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_40
qQC1_6 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_7
qQC0_20 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_21
qQC1_22 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_23
qQC0_10 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_11
qQC0_51 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_52
qQC0_9 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_10
qQC1_27 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_28
qQC0_15 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_16
qQC0_48 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_49
qQC1_31 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_32
qQC1_28 aF | aV15 | aV14 | aV13 | aV12 | aV11 | aV10 | aV9 | aV8 | aV7 | aV6 | !aV5 | !aV4 | aV3 | aV2 | aV1 | (aV0 & !aV0) | qQC1_29
qQC0_47 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_48
qQC0_6 !aF & !aV15 & !aV14 & !aV13 & !aV12 & !aV11 & !aV10 & !aV9 & !aV8 & !aV7 & !aV6 & aV5 & aV4 & !aV3 & !aV2 & !aV1 & (!aV0 | aV0) & qQC0_7

I run this code:

Mata::Mintermization mintermization;
auto mintermized_input = mintermization.mintermize(Mata::IntermediateAut::parse_from_mf(Mata::Parser::parse_mf(input))[0]);

where input is the string containing the AFA.

Some notes on the automata format

A few comments on the automata format:

What is meant by the "shared nodes" in the format?
What transition does a single a symbol or interval represent?
(a) The description of the format mentions complemented intervals as something that is not so needed. Well, I would very much vote for having them. In my experience with ARMC, the complemented sets were VERY useful.
(b) The current format uses "^" in the negated intervals, which is not mentioned among the special symbols: add or use "!" instead (which is, however, not so common).
(c) Also, I guess that classical sets of the form [abg-p] are not included since it is assumed that they would be replaced by multiple transitions. However, that stops working for negated sets: one cannot so easily encode things like [^abg-p]. Myself, I would vote for supporting classical sets as well as their negations (indeed, for many people writing something like [abc] or [^abc] is very usual).
How are initial states encoded?
Acceptance is done through transitions without a target state?
In the transducers:
(a) The description uses the notation x@a1 (also used at the beginning of the document when describing the basic notation), but the example uses a1@x.
(b) The example mixes symbols with tracks and without tracks. If a track is not specified, what does that mean?
What does the notation f"z=x" mean in the special transducer transitions? Can one use something like [a-z]"x=y" to say that the same symbol from [a-z] is read by both of the tracks?

Integrating code by Tomas Kocourek

This issue should be solved by Tomas Kocourek by integrating his implementation of AFA to the Mata library.

Create your own branch for development
Study library, especially the header and source files.
Compare your code to existing implementation and decide whether it is better to replace it completely or to somehow integrate it
Implement it.

Winter cleaning: Synchronize the mata with its usage in string solving and Z3

Lets try to start using the current mata from this git repo in the string solver.
What do we need to do?

I guess we first need to merge the pull requests, right? Ca we do it now? Lets not wait for every little thing to get fully resolved, is there perhaps a way to leave if for later?

Remove VM related source code

We should remove VM related source code. VM is not finished and we would need significant amount of work to finish it. @kilohsakul claims that these redundant source code could scare potential users of our library. Actually, it scares primarly him, however we should make him happy by removing VM.

Rename to mata

mata was chosen as a new name of this library. We need to:

1. Rename the project
2. Rename the namespaces in the source code
3. Find any other occurences of vata2 in the project files and rename it.
4. Hide forked from ondrik/libvata2. It is wanted by @kilohsakul, however I think that @ondrik will need to agree with this. I will contact github support which can remove the note about fork.

Fix Mata CMake configuration

The current CMake configuration should be modified and updated. Namely, the following should be done:

add a definition of install command to easily install Mata on the system,
create Mata CMake package which would allow using Mata in 3rd party projects with simple find_package(proj mata*) (*or libmata),
fix Mata compilation process to correctly link with simlib,
fix how Mata includes 3rd party dependencies so that Mata can be seamlessly used as a submodule with simple add_subdirectory (which will compile the whole Mata with its 3rd party dependencies) and allow linking the whole compiled library with target_link_libraries().

Failed to set the new version to file

After a merge, the following action fails.

Concatenation bug

I have the following code:

Mata::Nfa::Nfa aut1;
Mata::RE2Parser::create_nfa(&aut1, "a*");
Mata::Nfa::Nfa aut2;
Mata::RE2Parser::create_nfa(&aut2, "b*");
Mata::Nfa::Nfa aut3;
Mata::RE2Parser::create_nfa(&aut3, "a*b*");
Mata::Nfa::are_equivalent(Mata::Nfa::concatenate(aut1, aut2), aut3);

The equivalence check on the last line should be true, but it is not. It seems there is a problem in concatenation resulting in this case to the NFA accepting "(a|b)*".

Many type defs in nfa.hh

There are many named types "using ... that and that".
nfa.hh looks kind of scary.
My first guess is that it only makes the code harder to read, unles one memorises all of them.
I remember that we started with about five of them originally, in order to be able to swap the std containers in the nfa trnsition function.
I don't see why the other ones are there right now, in case there are really there for no big reason, then I woul dbe for dumping them.

AFA to NFA conversion

Add proper tests for regex parser

We need to add more tests for parser of regexes. Test the parser on more complex regexes and confirm that the parser gives correct automata.

Furthermore, it would be useful to add tests for the whole pipeline from smtlib to NFA.

We might be able to take inspiration from tests for RE2.

Fix an issue with mintermization of constants (true/false)

Constants that can occur in automata are not handled right now during mintermization.
For example , for this NFA:

@NFA-bits
%States-enum q r s
%Alphabet-auto
%Initial q
%Final r
q true r
r a1 & a2 s
s false s

the resulting mintermized NFA should have transitions from q to r for all minterms (created from the transition q true r), while there should be no transitions created from s false s.

For AFA, taking this example:

@AFA-bits
%Initial q0
%Final t
q0 (true & q2 & q3 & q0) | (a4 & !a5 & !a6 & !a7 & q0 & q1 & q2)
q1 false
q2 q1
q3 true

There will be two minterms: a4 & !a5 & !a6 & !a7 and its negation. Then, from q0 there should be two transitions (one for each minterm) in mintermized automaton going to q2 & q3 & q0 created from (true & q2 & q3 & q0) and one transition going to q0 & q1 & q2 with minterm representing a4 & !a5 & !a6 & !a7. From q1 there should be no transitions; the transition q2 q1 has the same meaning as q2 true & q1 and from q3 there will be two transitions (again, one for each minterm) going to true.

Remove NFA wrapper

Remove structure NfaWrapper.

Replace usages of the structure
Include alphabet and states dictionary directly to struct Nfa.

Add Python bindings for the new functions

With PRs #36, #40 and #41, there are multiple new functions needing Python bindings. Once #41 is reviewed and merged, we need to implement Python bindings for the new functions these PRs introduce.

The new functions which require Python bindings are:

Allow specifying an epsilon symbol when computing the shortest words

When shortest words are computed, Mata considers all symbols on transitions as normal symbols and adds them, if appropriate, to the sets of the shortest words for corresponding states.

However, if we have an automaton with some epsilon symbol and want to get the set of the shortest words for some states, we will get words with the epsilon symbol possibly included in the words. Furthermore, as epsilon transitions does not cost anything, the shortest words would not be computed correctly.

We decided that an epsilon symbol can be specified for some operations by passing an epsilon symbol to the corresponding function. Hence, we need to update the algorithm for getting the shortest words to optionally allow specifying an epsilon symbol to be passed to the function. The algorithm will then have to be updated to appropriately handle encountered epsilon symbols when computing the shortest words.

Implement parser for new automata format

Once a format specification is complete, we will need support at least for NFA and AFA parsing.

Rename strings to words

There are multiple occurrences where words (as in, sequences of symbols) are addressed by string: in user defined types, function names, local variables etc.

It has been decided that, for the matter of consistency, all such occurrences should be renamed to word. Furthermore, word does not collide with C++ string type.

Add return value type hints to Python binding

We should add return value type hints to all Python binding functions.

Resolve Mata compilation warnings

As time goes on and multiple Mata modules are implemented and modified (NFA, AFA, parser, etc.), the warnings returned by the compiler pile up. It becomes increasingly harder to search the build log for errors and meaningful warnings.

We should try to do some spring-cleaning a bit early in the year and fix as many warnings as possible. Write tests for unused functions, add (void) param in unimplemented functions and resolve other meaningful warnings so that it is easier for the developers to look through the build log and spot actually important warnings.

Resetting the version of mata (discussion)

Some, people complained, that it is strange to have 1.X.Y version of mata, since it is not finished.

Hence, I'm raising discussion, whether we should reset the version to 0.1.0, e.g. and continue with the clean state.

Technically, it should not be that hard.

Encapsulate state logic into isolate class

Make a special kind of container for properties of states?
To be used for initial, final states, various flags used in exlorations, searches.
It needs very fast test, addition, removal, and fast reset (emptying) would be also good.

A simple version - bool array indexed by statesis.
is_set(), set(i), reset(i), get_set() -- returns a vector of flagged states, perhaps get_not_set()
This is probably enough.
A more complex version also has an unordered vector of states that remembers which flags are set.
Test only tests the flag.
Insert sets the flag and pushes back the state to the vector.
Remove rests the flag, does nothing with the vector.
Reset iterates through the vector and resets flags of its states.
One shuold have the choice not to use the vector.
Even more complicated version replaces the unordered vector with something with easy removal in the middle, such as list. The flag can have a pointer to its occurence in this container, hence remove can go remove just that one element.
....

Encapsulate Delta.post_size() wherever possible

The library was so far based on determining number of states by checking size of post which is now implemented by method Delta.post_size(). Since we changed philosophy what number of states is we need to replace call to that method by Nfa.max_state().

Name of library

We should discuss and decide a new name of library.

Add documentation

Code is mostly undocumented, even interface in header files. It looks like a good idea to add documentation to code.

String variable NFA_TYPE defined in nfa.cc is empty.

The string variable NFA_TYPE defined here and declared here is always empty when used later in code. I compile code with clang in the following version

Apple clang version 13.1.6 (clang-1316.0.21.2.3)
Target: arm64-apple-darwin21.4.0
Thread model: posix

The error leads to failures in unit tests 11,13,14,40, since the NFA_TYPE is used in virtual machine to register dispatcher for NFA and no dispatcher is found for NFA the string empty.

Any ideas what could be wrong with the implementation?

P.S.:
I checked that the NFA_TYPE string is empty by adding the following print statment std::cout << "HERE "<< Vata2::Nfa::TYPE_NFA; to function Vata2::Nfa::init in the file src/nfa-dispatch.cc.

Upgrade to newer standard of C++

We are currently using C++14 standard. However, I believe we could benefit from the newer standards (C++20, or if C++20 support in compilers is not stable enough for us, C++17). Seeing as we do not need to use any particular specialities of C++20, I think it would be safe upgrading to C++20. Nevertheless, upgrading to at least C++17 should be completely safe. Is there any other reason why we have still remained on C++14 standard so far?

I myself wanted to use some methods on STL containers, yet because they were introduced in newer standards, I have to reimplement the functionality of these methods each time instead of simply calling them.

I have tested compilation of libMata with both C++17 and C++20 with g++ (GCC) 12.1.0. The library compiled without a problem and tests run successfully both times.

RE2 regex bug

When working with the regex parser (with python binding), I got the following fishy outcomes:
mata.Nfa.from_regex("[qQrR]*") yields
initial_states: [0] final_states: [0] transitions: 0-[113]→0 0-[114]→0

mata.Nfa.from_regex("[qr]*") yields the same automaton as before
initial_states: [0] final_states: [0] transitions: 0-[113]→0 0-[114]→0

Union of automata is not working

Function void uni (Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) is not working as expected.

I have replicated the issues in the following branch: hotfix-failing-union.

The minimal example does union of automaton accepting string 1 and automaton accepting the string 0. IMO the result should accept both 1 and 0, however, it does not accept 0. Printed automaton looks weird as well:

The test case that replicates the issue:

TEST_CASE("Vata2::Nfa::union_norename()") {
    Word one{1};
    Word zero{0};

    Nfa lhs(2);
    lhs.add_initial(0);
    lhs.add_trans(0, 0, 1);
    lhs.add_final(1);
    REQUIRE(!is_in_lang(lhs, one));
    REQUIRE(is_in_lang(lhs, zero));

    Nfa rhs(2);
    rhs.add_initial(0);
    rhs.add_trans(0, 1, 1);
    rhs.add_final(1);
    REQUIRE(is_in_lang(rhs, one));
    REQUIRE(!is_in_lang(rhs, zero));

    SECTION("failing minimal scenario") {
        Nfa result;
        uni(&result, lhs, rhs);
        REQUIRE(is_in_lang(result, one));
        REQUIRE(is_in_lang(result, zero));
    }
}

EDIT: My test cases for Ondra's implementation worked without problem (I tested little bit more complex automata, however, this minimal example should suffice).

Design a new CLI

We should:

write down requirements for a new CLI
design a solution
implement it

Separate .h and .cc for alphabets

To clean up nfa.h, and it is even needed since the same alphabets should be used in afa eventually.

Nondeterministic failure of macos github actions

Seems that macos build fails nondeterministically. Might be an issue, that they are slowly abandoning the current macos image and want to migrate to `macos121. Usually restarting the job fixes it.

Can someone with MacOS experience investigate and fix this?

See: https://github.com/VeriFIT/mata/actions/runs/3736376314/jobs/6340615433

The core of the problem seems to be:

[ 36%] Performing build step for 'cudd_library'
/Users/runner/work/mata/mata/3rdparty/cudd/build-aux/missing: line 81: aclocal-1.16: command not found
WARNING: 'aclocal-1.16' is missing on your system.

Add testing of the jupyter notebooks to github actions

Currently, the notebooks are not checked, and I fear they are out of sync with current changes.

Add its testing (wrt https://stackoverflow.com/questions/35471894/can-i-run-jupyter-notebook-cells-in-commandline) to github actions so we can fix it always right away.

Separate simulation to stand alone library.

It looks like a good idea to extract simulation to stand alone library which one can use also in other libraries and tools. We should discuss this.

Unify the logic of max states for Nfa, Delta, and Unary predicates

We decided that:

size() of Delta is number of triples in transition relation
add_trans should be method of Delta.
We need Delta and NumberPredicate to provide the function max_state() which returns maximal state used in them.
Implementation of the previous is an internal thing of the classes. Delta will probably need to keep internal counter of states where maximal state seen in lhs and rhs will be stored.
Nfa will have its own counter which will be increased by add_state()
Nfa will have method max_state() returning maximum of its own counter, and max states of initial, final states and delta.
The implementation will imply what states are. If there is a maximal state in initial predicate number 1000 but it is set to false, is it the state 1000 in automaton or not?

Implement or improve data structures for AFA

Missing automata operations

I am starting an issue with useful automata operations that could be included to the library.

trim removing redundant states (for some reason the regex translator generates many redundant states)
simulation-based minimization reduction of nondeterministic automata

Simple interface of functions such as is_included_antichain

Currently they have 5 parameters, three are not used.
Maybe make them optional?
The alphabet parameter should probably dissappear from inclusion and equivalence, regardless nfa having it as a property or not.
If there are more skeletons like this, we chould clean them.

Another issue related to user friendliness of these functions, I am still not sure wheter making more header files and more namespaces for these functions was a good idea. For me it gets hard to call these functions, I need to search for the right name space, include, use strange keyboard shortcuts in CLion, .... it is stressful for an old person. I can do it eventually, but it eats brain cycles. Not sure what is better here.

Remove revert function.

Remove revert function which is redundant.

RE to automata: desired behaviour?

When playing with the python binding providing a translation of REs to automata, I encountered an issue probably with a symbol representation. For instance, I would expect that the RE "\xff" is translated to an automaton accepting a single letter "255". In fact, the translator creates an automaton accepting the word "195.191" (attached). Not really sure, if such a behaviour is indeed desired.
aut3.dot.pdf

Fix the broken binding in devel

Current binding is broken, because of the merge of one of the PRs.

Disclaimer: I won't be fixxing any binding in any PR until this issue is solved (in isolate PR).

Currently, I'm waiting for merging of the Data encapsulation, which had working binding, and contains some changes that could lead to some conflict if I started fixing this and also will be handy in fixing the break from #100. Once #101 is merged, I will try to fix it.

Why do we need to denote formula in this special way? Would not it be sufficient to write formula to " "?

Originally posted by @martinhruska in #4 (comment)

Should add_trans() function throw exception or resize the automaton?

I am opening this issue for wider discussion.

Assume the following code:

lhs = Nfa();
lhs.add_trans(0,0,0);

In previous (Ondra's) implementation, this worked without problems: new transition was made, and 0 was added as a state of lhs.

However, the new implementation raises std::runtime_error: 0 or 0 is not a state.

Correct code is then:

lhs = Nfa(1);
lhs.add_trans(0,0,0);

lhs = Nfa();
lhs.increase_size(1);
lhs.add_trans(0,0,0);

The question I am rising is. Would you prefer:

Raising the error, if the automaton has not a proper/valid size
Quietly resize the automaton to include the new (unregistered) states?

Naming of things

Naming of files, _ or -?

Fix an issue with unhandled exception

The following code causes an unhandled exception (and I suppose it should not):

Mata::Nfa::Nfa aut;
Mata::RE2Parser::create_nfa(&aut, "(a|b)*");
Mata::Nfa::Nfa aut2;
Mata::RE2Parser::create_nfa(&aut2, "(a|b)*b(a*)b");
Mata::Nfa::are_equivalent(aut, aut2);

Can you please fix it?