Conditional input in verification property

[AWbosman]

Dear authors,

I am interested in verifying a property where the change a certain input variable can make is dependent on another. In a comment on an issue @MatthewDaggitt gave an example ( x0 +x1 <=1) and I was wondering whether this kind of property is currently supported by Marabou as I have not seen any examples of this.

Originally posted by @MatthewDaggitt in https://github.com/NeuralNetworkVerification/Marabou/issues/490#issuecomment-985397152

[wu-haoze]

Hi @AWbosman , Marabou supports general linear constraints over input variables. I usually prefer using the Python API: https://github.com/NeuralNetworkVerification/Marabou/blob/master/maraboupy/examples/7_PythonicAPI.py

Other front ends of Marabou (e.g., VNN_LIB parser) can also take constraints like that.

[AWbosman]

Hi wu-haoze,

Thanks for the quick reply! I will close the issue

EDIT: Could you direct me to an explanation on how to use a vnnlib file as veriifcation property with Marabou? I have a vnnlib as well as a network.

I have tried running command line like this : _Marabou opset_10nopad.onnx spec.vnnlib
There are no errors, but it runs forever and I cannot seem to set a timeout on commandline.

[wu-haoze]

@AWbosman , this is the right way to use it on the command line. ./Marabou --help will show the command line options, including timeout.

The long running time could be due to the sub-optimal implementation of the C++ onnx parser (#754 ) which we are trying to fix. For now, please use the Python API if you want to parse a ONNX network.

[wu-haoze]

Closing the issue due to inactivity. Feel free to re-open if needed.