sillydan1/aaltitoad

Extendable verification engine and simulator for Tick Tock Automata constructs

aaltitoad's Issues

linux: parsing suddenly stops

Describe the bug
In version v1.0.0, the expr parser switches to std::cin for some reason when compiled on linux

To Reproduce
Steps to reproduce the behavior:

1. Steal, Purchase or otherwise obtain a computer with Ubuntu 22.04 LTS
2. Clone and compile the verifier and hawk_parser targets
3. Run verifier -f /path/to/test/verification/fischer-suite/fischer2 -i ".*ignore.*" -v 6 -p hawk_parser
4. Observe that the parser stops in the middle of everything
5. If you press ctrl+d (EOF) the parser continues, but does not register the declaration.

Expected behavior
I expect that this shouldn't happen on any platform, let alone linux. The parser shouldn't switch to std::cin in the middle of a string.

Desktop (please complete the following information):

• OS: Ubuntu 22.04 LTS
• Version v1.0.0

Additional context
This is confirmed not to happen on macos - my guess is that there are slight differences in the flex/bison distributions which generates slightly different parser code.

The tool always returns 0

It should return non-zero when queries are not satisfied, or if parsing/other fails

Catch SIGTERM and handle it properly

When cancelling a verification job, it might be useful to get the data collected so far. e.g. solved queries and/or statistics on how many states have been explored so far etc.

Catching the SIGTERM interrupt signal would enable this sort of behavior to be implemented

Guards with parentheses that checks on interesting variables are not parsed properly

This may result in weird behavior if used.

Feature: CLI option for fileignore

Something like --ignore-files "REGEX"

Project Naming Discussion

Leave your name suggestions down below. These are my ideas so far:

• AALTITOAD (AAlborg TIck TOck Automata Debunker/Doublechecker/valiDator)
• TTAAAL (Tick Tock Automata AALborg)
• TAEBAAL - (Pronounced tea-ball) Ticktock Automata Engine By AALborg
• TETARVAAL (TTA Engine with Trace Abstraction Refinement Verification AALborg)
• TOTAAL (Tick tOck auTomata AALborg)

Or just something super boring such as

• ttaverif
• verifytta

Parsing of .parts files

.parts files have custom variable types. We need to figure out a way for users to specify these types and their runtime behaviour. (e.g. an output variable that needs doubles/strings/integers or even combinations of them)

We need an agreed upon syntax for these type-declarations.

The cparse library supports custom types, so maybe that'll fit in nicely there?

NOTE: We also need to mark variables as "internal"/"external[ I | O ]"

A G feature is still wrong

The flipped version of E F-queries has not been implemented correctly.

This is what happens when you code late at night

Codebase is messy

Some major refactoring are in order

Build packages for distribution

Currently, we are only shipping source releases. For better reach, we should provide package releases for debian/ubuntu, arch, (possibly) alpine, homebrew, and whatever windows uses. The package is technically available through CPM, but that is only relevant for other C++ developers and not for people who just want to use the tool suite.

This would preferably be done through a (series of) CI pipelines, with maybe a manual package-push step?

As an MVP implementation, we should just target one of the proposed distributions as a proof of concept and then introduce more and more distributions one by one.

CI for OSX and Windows

Getting CI up and running for platforms other than GNU/Linux would make this project much easier to get into. I have tried to get both osx and windows working, but I keep running into platform specific annoyances such as cmake's FindFLEX script not providing the FLEX_INCLUDE_DIR variable on macos and std::stringstream being implemented "wrong" in the msvcpp stl has been some really annoying roadblocks.

It would be best if we could officially support all platforms (osx, linux, windows and freebsd(maybe?))

I personally dont have much experience with github workflows and the limited tinkering I have done have given me a bad impression. If anyone can help by providing a PR with the workflows that would be really nice.

—output is doing nothing

Readme compile instructions is wrong

submodules are not initialized like it is explained right now. It should be:

git submodule update --init --recursive

... I think

Naive implementation in plugin system

The function bool is_dynamic_library(const std::string& filename) implementation is quite naïve in the sense that it just checks if the filename contains dylib/so/dll.

This means that a file named foo.so.txt is considered a dynamic library and is the program attempts to load it as a plug-in.

A real solution would be to use terminfo to inspect what the given file is.

Statistics to file / pipe

Feature Request: Output runtime statistics to CSV / pipe

Note: This request is based off of the implementation of v1.0.0. See #37 for dev progress

This could be toggled with a command line option e.g. --output-status /path/to/file. The output should/could be semicolon separated, making it easy to graph.

A usage example could be to output the waiting list size and passed list size to an output pipe with a plotting program receiving the data, you could graph the current state of the system.

Statistics may include:

• Waiting list size
• Passed list size
• Count of encountered hash-collissions
• How much memory is used (Could be limited with a cli option: --max-ram 16GiB report with OOM <stats>)
• Estimate of how far the search is (upper bound could be pre-calculated)
• Set a --max-time 30minutes that is simply checked during search. Report with DNF <stats>

This could be implemented as part of the traceable_multimap<T> class. There would have to be done some preliminary work on how to easily inject command-line options into the forward reachability search class

Statespace explosion handling on Tock is semantically incorrect

In TTASuccessorGenerator::GetNextTockStates, if the --explosion-limit is set to something, then the verification results might (and are very likely to) be incorrect.

Removing the --explosion-limit to begin with is definitely a good idea.

Integrating TAR via possibly the Z3 prover could also fix this problem

v1.0.0 reimplementation

If you have any questions or feature requests, please ask in the comments of this issue or submit a new issue.

Aaltitoad version 0.9.x is very messy and must be reimplemented, so that future development can be done.
These are the features of which the reimplementation should have.

Check branch major/reimplementation for progress on v1.0.0

v1.x.x Features

In addition to 0.9x features, version v1.0.0 should also have the following:

• All dependencies handled through CPM
• Plugin system for custom tocker programs
• Plugin system for model parsers
• Plugin system for syntax reducers/optimizers
• Out-of-the-box hawk parser (might be extracted into it's own project for maximum industry compatibility)
• Binary serialization/deserialization (might use cereal or yas. Will use this benchmark as main reference)
• A (code-wise) cleaner approach to storing the model in memory
• Transitioning git culture to conventional commits style

v1.0.0 milestones

• initial ticks implementation
• initial tocker implementation
• >80% coverage (tta.h/tta.cpp)
• Clear TODOs
• >80% coverage (interesting_tocker)
• >80% coverage (async_tocker)
• simulator integration
• throw out dead code
• Clear TODOs
• A new expr-based CTL parser
• Forward Reachability Search (E F p / A G p only - no subqueries to begin with)
• >80% coverage (FRS)
• NTTA json-project folder parser
• Create a verifier cli
• HAWK parser
  • scoped variable access per TTA instance
• Clear TODOs
• >80% coverage
• Release v1.0.0 🎉
• Write semantics algorithm(s) up in latex
• Write documentation (autodocs or github pages docs - will see when I get there)

Undecided features

• Trace Abstraction Refinement based verifier
• Binary Decision Diagram based verifier
• Binary serialization of TTAs

v0.x.x (current release) Features

• Forward Reachability Verifier
• Interestingness reduction
• A simulator (it's in there somewhere)

AG queries with counterexamples is doubly-inverted, which is confusing.

With AG queries, they are always "true" until you find a counter-example, then they are "false", but with a solution. Right now, we are doing the opposite.

In other words: AG queries (safety queries) should be disproven by finding a trace, not proven.

Solutions should be refactored to have:

struct query_answer_t {
  query_t q;
  std::optional<state_it_t> witnessing_state; // backtraceable - if optional is empty, no trace is availble (yet)
  bool witnessing_state_is_proof_of_unsat; // when true, then the query is _not_ satisfied
}

or something like that.

See forward_reachability_searcher.cpp:84