Skip to content

Automata learning algorithms - #480

Open
jkhav wants to merge 3 commits into
VeriFIT:develfrom
jkhav:learning
Open

Automata learning algorithms#480
jkhav wants to merge 3 commits into
VeriFIT:develfrom
jkhav:learning

Conversation

@jkhav

@jkhav jkhav commented Feb 1, 2025

Copy link
Copy Markdown

This PR includes implementation of L* and NL* automata learning algorithms for inferring DFA or RFSA from an unknown set.
https://people.eecs.berkeley.edu/~dawnsong/teaching/s10/papers/angluin87.pdf
https://www.ijcai.org/Proceedings/09/Papers/170.pdf

Note: I wasn't sure where this should belong in the library so I created a new file.

@Adda0

Adda0 commented Feb 3, 2025

Copy link
Copy Markdown
Collaborator

Hey. Thank you for the PR. It looks great. I will do a proper review when I have some time.

@Adda0
Adda0 requested review from Adda0 and ondrik February 3, 2025 10:36
@Adda0

Adda0 commented Feb 3, 2025

Copy link
Copy Markdown
Collaborator

@ondrik Could you have a quick look to confirm that the PR contains what you wanted?

Added new file learning.cc for L*, NL*
Added example program - use of learning
edited CMakeLists accordingly

Fixed a bug with rfsa_closure -- property violated when it shouldn't because of prime rows
evaluating of prime rows was fixed

@Adda0 Adda0 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall, it looks great. Thanks for the PR. As of now, I am not reviewing the feasibility of the implemented algorithm. I will leave that up to @ondrik. Other than that, here are some initial thoughts about the formal requirements on the introduced changes.

Comment on lines +13 to +17
using namespace mata::nfa;
using namespace mata;
using namespace std;
using namespace mata::utils;
using namespace mata::nfa::algorithms;

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Never use using directives in the header file. It poisons the namespace of any file where this header file is included.

#include <vector>
using namespace mata::nfa;
using namespace mata;
using namespace std;

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Global using namespace std; directive is generally considered a bad practice. Some projects allow this directive inside a function definition or a class definition, but in Mata, we never use this directive with std. It would be great if you could remove it and use the scope resolution operators std::.

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For now, this location is fine. We will move applications of Mata such as this into a separate subfolder in the future. Something like mata/app/learning/ and similar.

Comment on lines +25 to +32
ParameterMap params;
params["algorithm"] = "nlstar";
Nfa res1 = learn(aut, params);
res1.print_to_dot(std::cout);

params["algorithm"] = "lstar";
Nfa res2 = learn(aut, params);
res2.print_to_dot(std::cout);

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you add a comment explaining what is happening in this example?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All structures and classes should adhere to the UpperCamelCase naming convention.

* @return true if the word is accepted by teacher
* @return false if its not accepted
*/
bool membership_query(Nfa teacher, Word word);

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Boolean check should start with is_ prefix, or contains_, is_member(), or similar.

Comment on lines +257 to +258
* @brief Constructs a conjecture automaton
* first defines all the states of the conjecture,

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There needs to be an empty line after @brief to start a long description. Or you must specify the beginning of a new block using @....

*/
bool equivalence_query(Nfa teacher, Nfa conjecture, Word& cex);

Nfa learn(Nfa teacher, const ParameterMap& params);

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

learn_nfa_from_... or similar? I would try to use a more descriptive name.

Comment thread src/nfa/learning.cc
Comment on lines +13 to +14
Nfa conjecture;
OT table(alphabet, teacher, params);

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are there different spacings?

Comment thread src/nfa/learning.cc
Comment on lines +165 to +168
S.clear();
Splus.clear();
all.clear();
E.clear();

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The names of all of these structs should be more descriptive.

@Adda0 Adda0 Mar 25, 2025

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The entire contents of this header file should be inside a new namespace for learning the automata. Something like mata::nfa::learning or just mata::learning (if multiple automata are supposed to be learned in the future, not just (N/D)FAs), or use even more specific name in place of learning which is quite a lot general and does not convey well what is the namespace supposed to encapsulate.

@Adda0 Adda0 added the status:stale The PR's progress has stalled. label Jul 2, 2025
@Adda0
Adda0 deleted the branch VeriFIT:devel June 10, 2026 10:51
@Adda0 Adda0 closed this Jun 10, 2026
@Adda0 Adda0 reopened this Jun 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

status:stale The PR's progress has stalled.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants