Commit a28517d1 authored by Joshua Moerman's avatar Joshua Moerman
Browse files

Finalizes my results in a zip file

parent fa057f03
Submission for the RERS Challenge 2016
======================================
Joshua Moerman, Radboud University
moerman@science.ru.nl
# Approach
The The approach I took was very simple:
1. Compile the source code and consider it black box. Error states (in the
reachability problems) will output their error number.
2. Use black box learning/testing techniques to generate a model (formally: a
deterministic Mealy machine).
3. a For the LTL problems, convert the Mealy machine to some format NuSMV uses
and then check the properties (also had to be converted).
b For reachability problems: read off the outputs in the generated model
# Some details
The learning algorithm I used was TTT for Mealy machines (available in
LearnLib). The equivalence oracle was implemted with a randomized Wp method.
The learning setup was running for approximately one week. The LTL problems did
not generate any new hypotheses after 24h (so despite all the testing no new
counter examples were found), which makes me confident in the quality of the
model. The other problems, however, were still generating new hypotheses. So
I am confident the Mealy machines I learnt for these are not complete. To get
an idea of size, the Mealy machine learnt for Problem 11 has more than 20.000
states!
I implemented some scripts for converting the output of LearnLib to NuSMV
myself. If one is interested, please contact me. After the challenge I will
make the git repository public.
I did not try to do anything clever. I was simply curious how the current set
of tools we have handles this size of problems.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment