Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dev query logger #61

Merged
merged 46 commits into from
Oct 4, 2018

Conversation

clazarus
Copy link
Collaborator

@clazarus clazarus commented Jun 1, 2018

  • added InputQuery.saveQuery(filename) which serializes a query to a file
  • PiecewiseLinearConstraint:
    • Added pure virtual serializeToString() - requiring a serialize function for each type of plc
    • Added pure virtual PiecewiseLinearConstraint(string) - requiring a constructor that can deserialize
  • ReluConstraint:
    • implemented the corresponding functions
  • MaxConstraint:
    • implemented the corresponding functions
  • QueryLoader: Object that parses a serialized queries and produced an InputQuery
    • accompanied by a mock main to showcase usage
    • correct functionality has been verified by confirming idempotency of serialized queries (ie. serializing and query, loading it serializing it again results in same serialization)
  • TODO: In implementing this functionality we discovered that there is some unexplainable behavior with queries that are missing bounds on some variables. Preprocessing steps would appear to be responsible but InputQueries were inspected before preprocessing and so missing variable bounds should cause no issues.
  • thanks to @kjulian3 for providing initial query serializer.

clazarus added 13 commits May 24, 2018 22:23
- adding Kyle's printQuery()
- constraint serializers added
- relu serializer implemented
- max serializer implemented
- logger complete
- missing parser logic
- WIP: file parser
- todo: max parser
- issues with preprocessing
- deal with missing bounds
- clean up
@guykatzz
Copy link
Collaborator

guykatzz commented Jun 1, 2018

Hi Chris,
The Travis test seems to be failing, can you have a look?

- Mock serializeToString()
- Mock serial constructor
@clazarus
Copy link
Collaborator Author

clazarus commented Jun 1, 2018

Oh sorry, I hadn't noticed. I've added the corresponding functions to the MockConstraint.

@guykatzz
Copy link
Collaborator

guykatzz commented Jun 1, 2018

I did some editing and left a few comments, please have a look

… saveQuery() to use File.h instead of ofstream.
@clazarus
Copy link
Collaborator Author

clazarus commented Jun 3, 2018

Hi Guy, thank you for your comments. I have addressed all of them except for replacing ofstream with File.h I think doing this will require reimplementing most of the logic in loadQuery(), I am happy to do it if you consider it necessary. I was following the pattern from the original AcasNNet parser, is this incorrect?

@guykatzz
Copy link
Collaborator

guykatzz commented Jun 3, 2018

Hi Chris,
I did another round of editing. File.h is preferable because it has a lot of error handling already built in (and also for consistency and testing). I saw you're short on time, so I did the conversion for you, but there are still some Todos (I also didn't test the code at all. A couple of the Todos are actually to add unit tests Currently File.h doesn't have mock infrastructure, so I'll add that and then you can add the tests).

/*
Serializes the query to a file which can then be loaded using QueryLoader.
*/
void saveQuery( const std::string &fileName );
Copy link
Collaborator

Choose a reason for hiding this comment

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

Please use our String class instead of std::string

starts with "relu,".
What do you think?
*/

Copy link
Collaborator

Choose a reason for hiding this comment

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

This comment still needs addressing

Copy link
Collaborator

Choose a reason for hiding this comment

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

Addressed this issue.


TS_ASSERT_EQUALS( file->lastPath, "query.dump" );

delete inputQuery;
Copy link
Collaborator

Choose a reason for hiding this comment

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

This also still needs addressing

#include "ReluConstraint.h"

// TODO: add a unit test for a sanity check

Copy link
Collaborator

Choose a reason for hiding this comment

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

Another TODO

List<String> tokens = line.tokenize( "," );

// Todo: check something about the number of tokens

Copy link
Collaborator

Choose a reason for hiding this comment

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

TODO

equation.addAddend( coeff, varNo );
}
inputQuery.addEquation( equation );

Copy link
Collaborator

Choose a reason for hiding this comment

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

empty line

}
serializeConstraint = serializeConstraint.substring(0, serializeConstraint.length()-1);
//++it;

Copy link
Collaborator

Choose a reason for hiding this comment

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

Remove comment and empty line

}
else
{
// Todo: Unsupport constraint, add error handling
Copy link
Collaborator

Choose a reason for hiding this comment

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

TODO



PiecewiseLinearConstraint *constraint = NULL;
printf("Constraint: %u, Type: %s \n", i, coType.ascii());
Copy link
Collaborator

Choose a reason for hiding this comment

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

log()

{
// Todo: Unsupport constraint, add error handling
}

Copy link
Collaborator

Choose a reason for hiding this comment

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

Empty lines

Copy link
Collaborator

@ShantanuThakoor ShantanuThakoor left a comment

Choose a reason for hiding this comment

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

LGTM

@sparth95 sparth95 merged commit 7d32d56 into NeuralNetworkVerification:master Oct 4, 2018
@guykatzz
Copy link
Collaborator

guykatzz commented Oct 4, 2018

Hi Parth, Shantanu,
When changing the engine code, please let me have a chance to look at the pull request before merging.

Things look mostly in good shape. A few additional comments:
InputQuery.cpp: remove the 4 prints in line 251, or wrap them in a log() function as is done, e.g., in QueryLoader
MaxConstraint: new constructor: formatting (spaces, etc), error handling if values does not have at least 2 elements
ReluConstraint: new constructor: formatting, error handling if values does not have precisely 2 elements
QueryLoader.cpp: lots of formatting issues, check the number of tokens after line 125 same as you do in, e.g., line 69

Finally, there's the very important matter of unit tests:
Test_inputQuery: test_save_query() is still empty. Also, please add a testing suite for QueryLoader.

I haven't reverted the already-merged pull request, but please address these comments in the near future. If anything is unclear or if you need my help, don't hesitate to ask. I'll look at the MaxConstraint pull request next.

matanost pushed a commit that referenced this pull request Nov 2, 2021
* query logger
* Relu deserializer
* max constraint deserializer
* adding functions for tests
* Mock serializeToString()
* Mock serial constructor
* loadQuery() and saveQuery() to use File.h instead of ofstream.
* mock infrastructure for testing classes that use File
* Adding saveQuery function interface in python
* Updating make file
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants