we should have a flag to the Alloy cross-compiler which automatically imports a separate file, where we have stored the asserts and other verification tests we want to run against the model.
this way, as the FlowLog program evolves, we can continue to run the cross-compiler on the program, updating the Alloy code, but keeping the work we did to verify properties, etc.
we should have a flag to the Alloy cross-compiler which automatically imports a separate file, where we have stored the asserts and other verification tests we want to run against the model.
this way, as the FlowLog program evolves, we can continue to run the cross-compiler on the program, updating the Alloy code, but keeping the work we did to verify properties, etc.