Skip to content

API

ADA-VERONA

ADA-VERONA: Neural Network Robustness Analysis Framework

A framework for analyzing neural network robustness through verification and adversarial testing.

AttackEstimationModule

Bases: VerificationModule

A module for estimating the robustness of a model against adversarial attacks.

Source code in ada_verona/verification_module/attack_estimation_module.py 
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
class AttackEstimationModule(VerificationModule):
    """
    A module for estimating the robustness of a model against adversarial attacks.

    """

    def __init__(self, attack: Attack, top_k: int = 1) -> None:
        """
        Initialize the AttackEstimationModule with a specific attack.

        Args:
            attack (Attack): The attack to be used for robustness estimation.
            top_k: Number of top scores to take into account for checking the prediction.
        """
        self.attack = attack
        self.top_k = top_k
        self.name = f"AttackEstimationModule [{attack.name}, top-{top_k}]"

    def verify(self, verification_context: VerificationContext, epsilon: float) -> str | CompleteVerificationData:
        """
        Verify the robustness of the model within the given epsilon perturbation.

        Args:
            verification_context (VerificationContext): The context for verification, 
            including the model and data point.
            epsilon (float): The perturbation magnitude for the attack.

        Returns:
            str | CompleteVerificationData: The result of the verification,
                                either SAT or UNSAT, along with the duration.
        """

        if isinstance(verification_context.property_generator, One2AnyPropertyGenerator):
            # Check if the property generator is of type One2AnyPropertyGenerator

            start = time.time()  
            torch_model = verification_context.network.load_pytorch_model() 
            device = 'cuda' if torch.cuda.is_available() else 'cpu'  
            target = verification_context.data_point.label  
            target_on_device = torch.tensor([target], device=device)  
            data_on_device = verification_context.data_point.data.clone().detach().to(device)  
            perturbed_data = self.attack.execute(torch_model, data_on_device, target_on_device, epsilon)  

            output = torch_model(perturbed_data) 

            _, predicted_labels = torch.topk(output, self.top_k) 

            duration = time.time() - start 
            if target in predicted_labels:
                return CompleteVerificationData(result=VerificationResult.UNSAT, took=duration, 
                                                obtained_labels=predicted_labels)
            else:
                return CompleteVerificationData(result=VerificationResult.SAT, took=duration, 
                                                obtained_labels=predicted_labels)
        else:
            raise NotImplementedError("Currently, only one 2 any verification is implemented for adversarial attacks.")

__init__(attack, top_k=1)

Initialize the AttackEstimationModule with a specific attack.

Parameters:

Name Type Description Default
attack Attack

The attack to be used for robustness estimation.

 required
top_k int

Number of top scores to take into account for checking the prediction.

 1
Source code in ada_verona/verification_module/attack_estimation_module.py 
35
36
37
38
39
40
41
42
43
44
45
def __init__(self, attack: Attack, top_k: int = 1) -> None:
    """
    Initialize the AttackEstimationModule with a specific attack.

    Args:
        attack (Attack): The attack to be used for robustness estimation.
        top_k: Number of top scores to take into account for checking the prediction.
    """
    self.attack = attack
    self.top_k = top_k
    self.name = f"AttackEstimationModule [{attack.name}, top-{top_k}]"

verify(verification_context, epsilon)

Verify the robustness of the model within the given epsilon perturbation.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification,

required
epsilon float

The perturbation magnitude for the attack.

 required

Returns:

Type Description
str | CompleteVerificationData

str | CompleteVerificationData: The result of the verification, either SAT or UNSAT, along with the duration.
Source code in ada_verona/verification_module/attack_estimation_module.py 
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
def verify(self, verification_context: VerificationContext, epsilon: float) -> str | CompleteVerificationData:
    """
    Verify the robustness of the model within the given epsilon perturbation.

    Args:
        verification_context (VerificationContext): The context for verification, 
        including the model and data point.
        epsilon (float): The perturbation magnitude for the attack.

    Returns:
        str | CompleteVerificationData: The result of the verification,
                            either SAT or UNSAT, along with the duration.
    """

    if isinstance(verification_context.property_generator, One2AnyPropertyGenerator):
        # Check if the property generator is of type One2AnyPropertyGenerator

        start = time.time()  
        torch_model = verification_context.network.load_pytorch_model() 
        device = 'cuda' if torch.cuda.is_available() else 'cpu'  
        target = verification_context.data_point.label  
        target_on_device = torch.tensor([target], device=device)  
        data_on_device = verification_context.data_point.data.clone().detach().to(device)  
        perturbed_data = self.attack.execute(torch_model, data_on_device, target_on_device, epsilon)  

        output = torch_model(perturbed_data) 

        _, predicted_labels = torch.topk(output, self.top_k) 

        duration = time.time() - start 
        if target in predicted_labels:
            return CompleteVerificationData(result=VerificationResult.UNSAT, took=duration, 
                                            obtained_labels=predicted_labels)
        else:
            return CompleteVerificationData(result=VerificationResult.SAT, took=duration, 
                                            obtained_labels=predicted_labels)
    else:
        raise NotImplementedError("Currently, only one 2 any verification is implemented for adversarial attacks.")

BinarySearchEpsilonValueEstimator

Bases: EpsilonValueEstimator

A class to get the critical epsilon value using binary search.

Source code in ada_verona/epsilon_value_estimator/binary_search_epsilon_value_estimator.py 
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
class BinarySearchEpsilonValueEstimator(EpsilonValueEstimator):
    """
    A class to get the critical epsilon value using binary search.
    """

    def compute_epsilon_value(self, verification_context: VerificationContext) -> EpsilonValueResult:
        """
        Compute the epsilon value using binary search.

        Args:
            verification_context (VerificationContext): The context for verification.

        Returns:
            EpsilonValueResult: The result of the epsilon value estimation.
        """
        epsilon_status_list = [EpsilonStatus(x, None, None, self.verifier.name) for x in self.epsilon_value_list]

        start_time = time.time()
        highest_unsat_value, smallest_sat_value = self.binary_search(verification_context, epsilon_status_list)
        duration = time.time() - start_time
        epsilon_value_result = EpsilonValueResult(
            verification_context=verification_context,
            epsilon=highest_unsat_value,
            smallest_sat_value=smallest_sat_value,
            time=duration,
            verifier = self.verifier.name,
        )

        logger.info(
            f"Verification Context: {verification_context.get_dict_for_epsilon_result()}, "
            f"epsilon_result: {epsilon_value_result.epsilon}"  
        )
        return epsilon_value_result

    def get_highest_unsat(self, epsilon_status_list: list[EpsilonStatus]) -> float:
        """
        Get the highest UNSAT epsilon value from the list.

        Args:
            epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

        Returns:
            float: The highest UNSAT epsilon value.
        """
        highest_unsat = None
        if len([x.result for x in epsilon_status_list if x.result == VerificationResult.UNSAT]) > 0:
            highest_unsat = max(
                [index for index, x in enumerate(epsilon_status_list) if x.result == VerificationResult.UNSAT]
            )

        highest_unsat_value = epsilon_status_list[highest_unsat].value if highest_unsat is not None else 0

        return highest_unsat_value

    def get_smallest_sat(self, epsilon_status_list: list[EpsilonStatus]) -> float:
        """
        Get the smallest SAT epsilon value from the list.

        Args:
            epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

        Returns:
            float: The smallest SAT epsilon value.
        """
        try:
            max_epsilon_value = max([x.value for x in epsilon_status_list])
        except ValueError:
            return 0
        smallest_sat = None

        if len([x.result for x in epsilon_status_list if x.result == VerificationResult.SAT]) > 0:
            smallest_sat = min(
                [index for index, x in enumerate(epsilon_status_list) if x.result == VerificationResult.SAT]
            )

        smallest_sat_value = epsilon_status_list[smallest_sat].value if smallest_sat is not None else max_epsilon_value

        return smallest_sat_value

    def binary_search(
        self, verification_context: VerificationContext, epsilon_status_list: list[EpsilonStatus]
    ) -> float:
        """
        Perform binary search to find the highest UNSAT and smallest SAT epsilon values.

        Args:
            verification_context (VerificationContext): The context for verification.
            epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

        Returns:
            float: The highest UNSAT and smallest SAT epsilon values.
        """
        if len(epsilon_status_list) == 1:
            outcome = self.verifier.verify(verification_context, epsilon_status_list[0].value)
            epsilon_status_list[0].set_values(outcome)
            logger.debug(f"current epsilon value: {epsilon_status_list[0].result}, took: {epsilon_status_list[0].time}")
            verification_context.save_result(epsilon_status_list[0])
            if epsilon_status_list[0].result == VerificationResult.UNSAT:
                return epsilon_status_list[0].value, self.get_smallest_sat(epsilon_status_list)
            else:
                return 0, self.get_smallest_sat(epsilon_status_list)

        first = 0
        last = len(epsilon_status_list) - 1

        while first <= last:
            midpoint = (first + last) // 2

            if not epsilon_status_list[midpoint].result:
                outcome = self.verifier.verify(verification_context, epsilon_status_list[midpoint].value)
                epsilon_status_list[midpoint].set_values(outcome)
                verification_context.save_result(epsilon_status_list[midpoint])
                logger.debug(
                    f"current epsilon value: {epsilon_status_list[midpoint].result},"
                    "took: {epsilon_status_list[midpoint].time}"  
                )

            if epsilon_status_list[midpoint].result == VerificationResult.UNSAT:
                first = midpoint + 1
            elif epsilon_status_list[midpoint].result == VerificationResult.SAT:
                last = midpoint - 1
            else:
                epsilon_status_list.pop(midpoint)
                last = last - 1

        logger.debug(f"epsilon status list: {[(x.value, x.result, x.time) for x in epsilon_status_list]}")

        highest_unsat_value = self.get_highest_unsat(epsilon_status_list)
        smallest_sat_value = self.get_smallest_sat(epsilon_status_list)

        return highest_unsat_value, smallest_sat_value

Perform binary search to find the highest UNSAT and smallest SAT epsilon values.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification.

 required
epsilon_status_list list[EpsilonStatus]

The list of epsilon statuses.

 required

Returns:

Name Type Description
float float

The highest UNSAT and smallest SAT epsilon values.
Source code in ada_verona/epsilon_value_estimator/binary_search_epsilon_value_estimator.py 
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
def binary_search(
    self, verification_context: VerificationContext, epsilon_status_list: list[EpsilonStatus]
) -> float:
    """
    Perform binary search to find the highest UNSAT and smallest SAT epsilon values.

    Args:
        verification_context (VerificationContext): The context for verification.
        epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

    Returns:
        float: The highest UNSAT and smallest SAT epsilon values.
    """
    if len(epsilon_status_list) == 1:
        outcome = self.verifier.verify(verification_context, epsilon_status_list[0].value)
        epsilon_status_list[0].set_values(outcome)
        logger.debug(f"current epsilon value: {epsilon_status_list[0].result}, took: {epsilon_status_list[0].time}")
        verification_context.save_result(epsilon_status_list[0])
        if epsilon_status_list[0].result == VerificationResult.UNSAT:
            return epsilon_status_list[0].value, self.get_smallest_sat(epsilon_status_list)
        else:
            return 0, self.get_smallest_sat(epsilon_status_list)

    first = 0
    last = len(epsilon_status_list) - 1

    while first <= last:
        midpoint = (first + last) // 2

        if not epsilon_status_list[midpoint].result:
            outcome = self.verifier.verify(verification_context, epsilon_status_list[midpoint].value)
            epsilon_status_list[midpoint].set_values(outcome)
            verification_context.save_result(epsilon_status_list[midpoint])
            logger.debug(
                f"current epsilon value: {epsilon_status_list[midpoint].result},"
                "took: {epsilon_status_list[midpoint].time}"  
            )

        if epsilon_status_list[midpoint].result == VerificationResult.UNSAT:
            first = midpoint + 1
        elif epsilon_status_list[midpoint].result == VerificationResult.SAT:
            last = midpoint - 1
        else:
            epsilon_status_list.pop(midpoint)
            last = last - 1

    logger.debug(f"epsilon status list: {[(x.value, x.result, x.time) for x in epsilon_status_list]}")

    highest_unsat_value = self.get_highest_unsat(epsilon_status_list)
    smallest_sat_value = self.get_smallest_sat(epsilon_status_list)

    return highest_unsat_value, smallest_sat_value

compute_epsilon_value(verification_context)

Compute the epsilon value using binary search.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification.

 required

Returns:

Name Type Description
EpsilonValueResult EpsilonValueResult

The result of the epsilon value estimation.
Source code in ada_verona/epsilon_value_estimator/binary_search_epsilon_value_estimator.py 
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
def compute_epsilon_value(self, verification_context: VerificationContext) -> EpsilonValueResult:
    """
    Compute the epsilon value using binary search.

    Args:
        verification_context (VerificationContext): The context for verification.

    Returns:
        EpsilonValueResult: The result of the epsilon value estimation.
    """
    epsilon_status_list = [EpsilonStatus(x, None, None, self.verifier.name) for x in self.epsilon_value_list]

    start_time = time.time()
    highest_unsat_value, smallest_sat_value = self.binary_search(verification_context, epsilon_status_list)
    duration = time.time() - start_time
    epsilon_value_result = EpsilonValueResult(
        verification_context=verification_context,
        epsilon=highest_unsat_value,
        smallest_sat_value=smallest_sat_value,
        time=duration,
        verifier = self.verifier.name,
    )

    logger.info(
        f"Verification Context: {verification_context.get_dict_for_epsilon_result()}, "
        f"epsilon_result: {epsilon_value_result.epsilon}"  
    )
    return epsilon_value_result

get_highest_unsat(epsilon_status_list)

Get the highest UNSAT epsilon value from the list.

Parameters:

Name Type Description Default
epsilon_status_list list[EpsilonStatus]

The list of epsilon statuses.

 required

Returns:

Name Type Description
float float

The highest UNSAT epsilon value.
Source code in ada_verona/epsilon_value_estimator/binary_search_epsilon_value_estimator.py 
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
def get_highest_unsat(self, epsilon_status_list: list[EpsilonStatus]) -> float:
    """
    Get the highest UNSAT epsilon value from the list.

    Args:
        epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

    Returns:
        float: The highest UNSAT epsilon value.
    """
    highest_unsat = None
    if len([x.result for x in epsilon_status_list if x.result == VerificationResult.UNSAT]) > 0:
        highest_unsat = max(
            [index for index, x in enumerate(epsilon_status_list) if x.result == VerificationResult.UNSAT]
        )

    highest_unsat_value = epsilon_status_list[highest_unsat].value if highest_unsat is not None else 0

    return highest_unsat_value

get_smallest_sat(epsilon_status_list)

Get the smallest SAT epsilon value from the list.

Parameters:

Name Type Description Default
epsilon_status_list list[EpsilonStatus]

The list of epsilon statuses.

 required

Returns:

Name Type Description
float float

The smallest SAT epsilon value.
Source code in ada_verona/epsilon_value_estimator/binary_search_epsilon_value_estimator.py 
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
def get_smallest_sat(self, epsilon_status_list: list[EpsilonStatus]) -> float:
    """
    Get the smallest SAT epsilon value from the list.

    Args:
        epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

    Returns:
        float: The smallest SAT epsilon value.
    """
    try:
        max_epsilon_value = max([x.value for x in epsilon_status_list])
    except ValueError:
        return 0
    smallest_sat = None

    if len([x.result for x in epsilon_status_list if x.result == VerificationResult.SAT]) > 0:
        smallest_sat = min(
            [index for index, x in enumerate(epsilon_status_list) if x.result == VerificationResult.SAT]
        )

    smallest_sat_value = epsilon_status_list[smallest_sat].value if smallest_sat is not None else max_epsilon_value

    return smallest_sat_value

EpsilonStatus dataclass

A class to represent the status of the verification. It records the epsilon value, the result (SAT, UNSAT, TIMEOUT, ERROR) and running time.

Source code in ada_verona/database/epsilon_status.py 
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
@dataclass
class EpsilonStatus:
    """
    A class to represent the status of the verification.
    It records the epsilon value, the result (SAT, UNSAT, TIMEOUT, ERROR) and running time.
    """

    value: float
    result: VerificationResult | None
    time: float = None
    verifier: str = None
    obtained_labels: list[int] = None

    def set_values(self, complete_verification_data: CompleteVerificationData):
        """
        Set values from the CompleteVerificationData

        Args:
            complete_verification_data: CompleteVerificationData
        """
        self.result = complete_verification_data.result
        self.time = complete_verification_data.took
        self.obtained_labels = complete_verification_data.obtained_labels

    def to_dict(self) -> dict:
        """
        Convert the EpsilonStatus to a dictionary.

        Returns:
            dict: The dictionary representation of the EpsilonStatus.
        """
        return dict(epsilon_value=self.value, result=self.result, time=self.time, verifier=self.verifier, 
                    obtained_labels=self.obtained_labels.flatten().tolist() if self.obtained_labels is not None 
                    else None)

set_values(complete_verification_data)

Set values from the CompleteVerificationData

Parameters:

Name Type Description Default
complete_verification_data CompleteVerificationData

CompleteVerificationData

 required
Source code in ada_verona/database/epsilon_status.py 
34
35
36
37
38
39
40
41
42
43
def set_values(self, complete_verification_data: CompleteVerificationData):
    """
    Set values from the CompleteVerificationData

    Args:
        complete_verification_data: CompleteVerificationData
    """
    self.result = complete_verification_data.result
    self.time = complete_verification_data.took
    self.obtained_labels = complete_verification_data.obtained_labels

to_dict()

Convert the EpsilonStatus to a dictionary.

Returns:

Name Type Description
dict dict

The dictionary representation of the EpsilonStatus.
Source code in ada_verona/database/epsilon_status.py 
45
46
47
48
49
50
51
52
53
54
def to_dict(self) -> dict:
    """
    Convert the EpsilonStatus to a dictionary.

    Returns:
        dict: The dictionary representation of the EpsilonStatus.
    """
    return dict(epsilon_value=self.value, result=self.result, time=self.time, verifier=self.verifier, 
                obtained_labels=self.obtained_labels.flatten().tolist() if self.obtained_labels is not None 
                else None)

EpsilonValueEstimator

Bases: ABC

An abstract base class for estimating epsilon values.

Source code in ada_verona/epsilon_value_estimator/epsilon_value_estimator.py 
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
class EpsilonValueEstimator(ABC):
    """
    An abstract base class for estimating epsilon values.
    """

    def __init__(self, epsilon_value_list: list[float], verifier: VerificationModule) -> None:
        """
        Initialize the EpsilonValueEstimator with the given epsilon value list and verifier.

        Args:
            epsilon_value_list (list[float]): The list of epsilon values to estimate.
            verifier (VerificationModule): The verifier to use for verification.
        """
        self.epsilon_value_list = epsilon_value_list
        self.verifier = verifier

    @abstractmethod
    def compute_epsilon_value(self, verification_context: VerificationContext) -> EpsilonValueResult:
        """
        Compute the epsilon value for the given verification context.

        Args:
            verification_context (VerificationContext): The context for verification.

        Returns:
            EpsilonValueResult: The result of the epsilon value estimation.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

__init__(epsilon_value_list, verifier)

Initialize the EpsilonValueEstimator with the given epsilon value list and verifier.

Parameters:

Name Type Description Default
epsilon_value_list list[float]

The list of epsilon values to estimate.

 required
verifier VerificationModule

The verifier to use for verification.

 required
Source code in ada_verona/epsilon_value_estimator/epsilon_value_estimator.py 
28
29
30
31
32
33
34
35
36
37
def __init__(self, epsilon_value_list: list[float], verifier: VerificationModule) -> None:
    """
    Initialize the EpsilonValueEstimator with the given epsilon value list and verifier.

    Args:
        epsilon_value_list (list[float]): The list of epsilon values to estimate.
        verifier (VerificationModule): The verifier to use for verification.
    """
    self.epsilon_value_list = epsilon_value_list
    self.verifier = verifier

compute_epsilon_value(verification_context) abstractmethod

Compute the epsilon value for the given verification context.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification.

 required

Returns:

Name Type Description
EpsilonValueResult EpsilonValueResult

The result of the epsilon value estimation.
Source code in ada_verona/epsilon_value_estimator/epsilon_value_estimator.py 
39
40
41
42
43
44
45
46
47
48
49
50
@abstractmethod
def compute_epsilon_value(self, verification_context: VerificationContext) -> EpsilonValueResult:
    """
    Compute the epsilon value for the given verification context.

    Args:
        verification_context (VerificationContext): The context for verification.

    Returns:
        EpsilonValueResult: The result of the epsilon value estimation.
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

EpsilonValueResult dataclass

A dataclass defining the verification result of a single verification.

Source code in ada_verona/database/epsilon_value_result.py 
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
@dataclass
class EpsilonValueResult:
    """
    A dataclass defining the verification result of a single verification.
    """

    verification_context: VerificationContext
    epsilon: float
    smallest_sat_value: float
    time: float = None
    verifier: str = None

    def to_dict(self) -> dict:
        """
        Convert the EpsilonValueResult to a dictionary.

        Returns:
            dict: The dictionary representation of the EpsilonValueResult.
        """
        ret = dict(
            **self.verification_context.get_dict_for_epsilon_result(),
            epsilon_value=self.epsilon,
            smallest_sat_value=self.smallest_sat_value,
            total_time=self.time,
            verifier=self.verifier,
        )
        return ret

to_dict()

Convert the EpsilonValueResult to a dictionary.

Returns:

Name Type Description
dict dict

The dictionary representation of the EpsilonValueResult.
Source code in ada_verona/database/epsilon_value_result.py 
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
def to_dict(self) -> dict:
    """
    Convert the EpsilonValueResult to a dictionary.

    Returns:
        dict: The dictionary representation of the EpsilonValueResult.
    """
    ret = dict(
        **self.verification_context.get_dict_for_epsilon_result(),
        epsilon_value=self.epsilon,
        smallest_sat_value=self.smallest_sat_value,
        total_time=self.time,
        verifier=self.verifier,
    )
    return ret

ExperimentRepository

Database to handle all the paths to the different files used.

Source code in ada_verona/database/experiment_repository.py 
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
class ExperimentRepository:
    """
    Database to handle all the paths to the different files used.
    """

    def __init__(self, base_path: Path, network_folder: Path) -> None:
        """
        Initialize the ExperimentRepository with the base path and network folder.

        Args:
            base_path (Path): The base path for the experiment repository.
            network_folder (Path): The folder containing the network files.
        """
        self.act_experiment_path = None
        self.base_path = base_path
        self.network_folder = network_folder

    def get_act_experiment_path(self) -> Path:
        """
        Get the path to the active experiment.

        Returns:
            Path: The path to the active experiment.

        Raises:
            Exception: If no experiment is loaded.
        """
        if self.act_experiment_path is not None:
            return self.act_experiment_path
        else:
            raise Exception("No experiment loaded")

    def get_results_path(self) -> Path:
        """
        Get the path to the results folder of the active experiment.

        Returns:
            Path: The path to the results folder.
        """
        return self.get_act_experiment_path() / "results"

    def get_tmp_path(self) -> Path:
        """
        Get the path to the temporary folder of the active experiment.

        Returns:
            Path: The path to the temporary folder.
        """
        return self.get_act_experiment_path() / "tmp"

    def initialize_new_experiment(self, experiment_name: str) -> None:
        """
        Initialize a new experiment with the given name.

        Args:
            experiment_name (str): The name of the experiment.

        Raises:
            Exception: If a directory with the same name already exists.
        """
        now = datetime.now()
        now_string = now.strftime("%d-%m-%Y+%H_%M")

        self.act_experiment_path = self.base_path / f"{experiment_name}_{now_string}"

        if os.path.exists(self.get_results_path()):
            raise Exception(
                "Error, there is already a directory with results with the same name,"
                "make sure no results will be overwritten"  
            )
        else:
            os.makedirs(self.get_results_path())
        os.makedirs(self.get_tmp_path())

    def load_experiment(self, experiment_name: str) -> None:
        """
        Load an existing experiment with the given name.

        Args:
            experiment_name (str): The name of the experiment.
        """
        self.act_experiment_path = self.base_path / experiment_name

    def save_configuration(self, data: dict) -> None:
        """
        Save the configuration data to a JSON file.

        Args:
            data (dict): The configuration data to save.
        """
        with open(self.get_act_experiment_path() / "configuration.json", "w") as outfile:
            json.dump(data, outfile)

    def get_network_list(self) -> list[ONNXNetwork]:
        """
        Return a list of networks by scanning
        the network folder for ONNX files if a network folder is given.

        Returns:
            list[Network]: The list of networks.
        """
        if self.network_folder is None:
            raise Exception("No Network folder given.")
        else:
            network_path_list = [file for file in self.network_folder.iterdir()]
            network_list = [ONNXNetwork(x) for x in network_path_list]
        return network_list

    def save_results(self, results: list[EpsilonValueResult]) -> None:
        """
        Save the list of epsilon value results to a CSV file.

        Args:
            results (list[EpsilonValueResult]): The list of epsilon value results to save.
        """
        result_df = pd.DataFrame([x.to_dict() for x in results])
        result_df.to_csv(self.get_results_path() / DEFAULT_RESULT_CSV_NAME)

    def save_result(self, result: EpsilonValueResult) -> None:
        """
        Save a single epsilon value result to the CSV file.

        Args:
            result (EpsilonValueResult): The epsilon value result to save.
        """
        result_df_path = self.get_results_path() / DEFAULT_RESULT_CSV_NAME
        if result_df_path.exists():
            df = pd.read_csv(result_df_path, index_col=0)
            df.loc[len(df.index)] = result.to_dict()
        else:
            df = pd.DataFrame([result.to_dict()])
        df.to_csv(result_df_path)

    def get_file_name(self, file: Path) -> str:
        """
        Get the name of the file without the extension.

        Args:
            file (Path): The file path.

        Returns:
            str: The name of the file without the extension.
        """
        return file.name.split(".")[0]

    def create_verification_context(
        self, network: Network, data_point: DataPoint, property_generator: PropertyGenerator
    ) -> VerificationContext:
        """
        Create a verification context for the given network, data point, and property generator.

        Args:
            network (Network): The network to verify.
            data_point (DataPoint): The data point to verify.
            property_generator (PropertyGenerator): The property generator to use.

        Returns:
            VerificationContext: The created verification context.
        """
        tmp_path = self.get_tmp_path() / f"{network.name}" / f"image_{data_point.id}"
        return VerificationContext(network, data_point, tmp_path, property_generator)

    def get_result_df(self) -> pd.DataFrame:
        """
        Get the result DataFrame from the results CSV file.

        Returns:
            pd.DataFrame: The result DataFrame.

        Raises:
            Exception: If no result file is found.
        """
        result_df_path = self.get_results_path() / DEFAULT_RESULT_CSV_NAME
        if result_df_path.exists():
            df = pd.read_csv(result_df_path, index_col=0)
            df["network"] = df.network_path.str.split("/").apply(lambda x: x[-1]).apply(lambda x: x.split(".")[0])

            return df
        else:
            raise Exception(f"Error, no result file found at {result_df_path}")

    def get_per_epsilon_result_df(self) -> pd.DataFrame:
        """
        Get the per-epsilon result DataFrame from the temporary folder.

        Returns:
            pd.DataFrame: The per-epsilon result DataFrame.
        """
        per_epsilon_result_df_name = "epsilons_df.csv"
        df = pd.DataFrame()
        network_folders = [x for x in self.get_tmp_path().iterdir()]
        for network_folder in network_folders:
            images_folders = [x for x in network_folders[0].iterdir()]
            for image_folder in images_folders:
                t_df = pd.read_csv(image_folder / per_epsilon_result_df_name, index_col=0)
                t_df["network"] = network_folder.name
                t_df["image"] = image_folder.name
                df = pd.concat([df, t_df])
        return df

    def save_per_epsilon_result_df(self) -> None:
        """
        Save the per-epsilon result DataFrame to a CSV file.
        """
        per_epsilon_result_df = self.get_per_epsilon_result_df()
        per_epsilon_result_df.to_csv(self.get_results_path() / PER_EPSILON_RESULT_CSV_NAME)

    def save_plots(self) -> None:
        """
        Save the plots generated from the result DataFrame.
        """
        df = self.get_result_df()
        report_creator = ReportCreator(df)
        hist_figure = report_creator.create_hist_figure()
        hist_figure.savefig(self.get_results_path() / "hist_figure.png", bbox_inches="tight")

        boxplot = report_creator.create_box_figure()
        boxplot.savefig(self.get_results_path() / "boxplot.png", bbox_inches="tight")

        kde_figure = report_creator.create_kde_figure()
        kde_figure.savefig(self.get_results_path() / "kde_plot.png", bbox_inches="tight")

        ecdf_figure = report_creator.create_ecdf_figure()
        ecdf_figure.savefig(self.get_results_path() / "ecdf_plot.png", bbox_inches="tight")

    def save_verification_context_to_yaml(self, file_path: Path, verification_context: VerificationContext) -> Path:
        """
        Save the verification context to a YAML file.

        Args:
            file_path (Path): The path to save the YAML file.
            verification_context (VerificationContext): The verification context to save.

        Returns:
            Path: The path to the saved YAML file.
        """
        with open(file_path, "w") as file:
            yaml.dump(verification_context.to_dict(), file)
        return file_path

    def load_verification_context_from_yaml(self, file_path: Path) -> VerificationContext:
        """
        Load the verification context from a YAML file.

        Args:
            file_path (Path): The path to the YAML file.

        Returns:
            VerificationContext: The loaded verification context.
        """
        with open(file_path) as file:
            data = yaml.safe_load(file)
            return VerificationContext.from_dict(data)

    def cleanup_tmp_directory(self):
        """
        Delete the temporary folder of the active experiment.
        """

        tmp_path = self.get_tmp_path()
        if tmp_path.exists():
            for file in tmp_path.iterdir():
                file.unlink()
            tmp_path.rmdir()

__init__(base_path, network_folder)

Initialize the ExperimentRepository with the base path and network folder.

Parameters:

Name Type Description Default
base_path Path

The base path for the experiment repository.

 required
network_folder Path

The folder containing the network files.

 required
Source code in ada_verona/database/experiment_repository.py 
41
42
43
44
45
46
47
48
49
50
51
def __init__(self, base_path: Path, network_folder: Path) -> None:
    """
    Initialize the ExperimentRepository with the base path and network folder.

    Args:
        base_path (Path): The base path for the experiment repository.
        network_folder (Path): The folder containing the network files.
    """
    self.act_experiment_path = None
    self.base_path = base_path
    self.network_folder = network_folder

cleanup_tmp_directory()

Delete the temporary folder of the active experiment.

Source code in ada_verona/database/experiment_repository.py 
290
291
292
293
294
295
296
297
298
299
def cleanup_tmp_directory(self):
    """
    Delete the temporary folder of the active experiment.
    """

    tmp_path = self.get_tmp_path()
    if tmp_path.exists():
        for file in tmp_path.iterdir():
            file.unlink()
        tmp_path.rmdir()

create_verification_context(network, data_point, property_generator)

Create a verification context for the given network, data point, and property generator.

Parameters:

Name Type Description Default
network Network

The network to verify.

 required
data_point DataPoint

The data point to verify.

 required
property_generator PropertyGenerator

The property generator to use.

 required

Returns:

Name Type Description
VerificationContext VerificationContext

The created verification context.
Source code in ada_verona/database/experiment_repository.py 
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
def create_verification_context(
    self, network: Network, data_point: DataPoint, property_generator: PropertyGenerator
) -> VerificationContext:
    """
    Create a verification context for the given network, data point, and property generator.

    Args:
        network (Network): The network to verify.
        data_point (DataPoint): The data point to verify.
        property_generator (PropertyGenerator): The property generator to use.

    Returns:
        VerificationContext: The created verification context.
    """
    tmp_path = self.get_tmp_path() / f"{network.name}" / f"image_{data_point.id}"
    return VerificationContext(network, data_point, tmp_path, property_generator)

get_act_experiment_path()

Get the path to the active experiment.

Returns:

Name Type Description
Path Path

The path to the active experiment.

Raises:

Type Description
Exception

If no experiment is loaded.
Source code in ada_verona/database/experiment_repository.py 
53
54
55
56
57
58
59
60
61
62
63
64
65
66
def get_act_experiment_path(self) -> Path:
    """
    Get the path to the active experiment.

    Returns:
        Path: The path to the active experiment.

    Raises:
        Exception: If no experiment is loaded.
    """
    if self.act_experiment_path is not None:
        return self.act_experiment_path
    else:
        raise Exception("No experiment loaded")

get_file_name(file)

Get the name of the file without the extension.

Parameters:

Name Type Description Default
file Path

The file path.

 required

Returns:

Name Type Description
str str

The name of the file without the extension.
Source code in ada_verona/database/experiment_repository.py 
169
170
171
172
173
174
175
176
177
178
179
def get_file_name(self, file: Path) -> str:
    """
    Get the name of the file without the extension.

    Args:
        file (Path): The file path.

    Returns:
        str: The name of the file without the extension.
    """
    return file.name.split(".")[0]

get_network_list()

Return a list of networks by scanning the network folder for ONNX files if a network folder is given.

Returns:

Type Description
list[ONNXNetwork]

list[Network]: The list of networks.
Source code in ada_verona/database/experiment_repository.py 
129
130
131
132
133
134
135
136
137
138
139
140
141
142
def get_network_list(self) -> list[ONNXNetwork]:
    """
    Return a list of networks by scanning
    the network folder for ONNX files if a network folder is given.

    Returns:
        list[Network]: The list of networks.
    """
    if self.network_folder is None:
        raise Exception("No Network folder given.")
    else:
        network_path_list = [file for file in self.network_folder.iterdir()]
        network_list = [ONNXNetwork(x) for x in network_path_list]
    return network_list

get_per_epsilon_result_df()

Get the per-epsilon result DataFrame from the temporary folder.

Returns:

Type Description
DataFrame

pd.DataFrame: The per-epsilon result DataFrame.
Source code in ada_verona/database/experiment_repository.py 
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
def get_per_epsilon_result_df(self) -> pd.DataFrame:
    """
    Get the per-epsilon result DataFrame from the temporary folder.

    Returns:
        pd.DataFrame: The per-epsilon result DataFrame.
    """
    per_epsilon_result_df_name = "epsilons_df.csv"
    df = pd.DataFrame()
    network_folders = [x for x in self.get_tmp_path().iterdir()]
    for network_folder in network_folders:
        images_folders = [x for x in network_folders[0].iterdir()]
        for image_folder in images_folders:
            t_df = pd.read_csv(image_folder / per_epsilon_result_df_name, index_col=0)
            t_df["network"] = network_folder.name
            t_df["image"] = image_folder.name
            df = pd.concat([df, t_df])
    return df

get_result_df()

Get the result DataFrame from the results CSV file.

Returns:

Type Description
DataFrame

pd.DataFrame: The result DataFrame.

Raises:

Type Description
Exception

If no result file is found.
Source code in ada_verona/database/experiment_repository.py 
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
def get_result_df(self) -> pd.DataFrame:
    """
    Get the result DataFrame from the results CSV file.

    Returns:
        pd.DataFrame: The result DataFrame.

    Raises:
        Exception: If no result file is found.
    """
    result_df_path = self.get_results_path() / DEFAULT_RESULT_CSV_NAME
    if result_df_path.exists():
        df = pd.read_csv(result_df_path, index_col=0)
        df["network"] = df.network_path.str.split("/").apply(lambda x: x[-1]).apply(lambda x: x.split(".")[0])

        return df
    else:
        raise Exception(f"Error, no result file found at {result_df_path}")

get_results_path()

Get the path to the results folder of the active experiment.

Returns:

Name Type Description
Path Path

The path to the results folder.
Source code in ada_verona/database/experiment_repository.py 
68
69
70
71
72
73
74
75
def get_results_path(self) -> Path:
    """
    Get the path to the results folder of the active experiment.

    Returns:
        Path: The path to the results folder.
    """
    return self.get_act_experiment_path() / "results"

get_tmp_path()

Get the path to the temporary folder of the active experiment.

Returns:

Name Type Description
Path Path

The path to the temporary folder.
Source code in ada_verona/database/experiment_repository.py 
77
78
79
80
81
82
83
84
def get_tmp_path(self) -> Path:
    """
    Get the path to the temporary folder of the active experiment.

    Returns:
        Path: The path to the temporary folder.
    """
    return self.get_act_experiment_path() / "tmp"

initialize_new_experiment(experiment_name)

Initialize a new experiment with the given name.

Parameters:

Name Type Description Default
experiment_name str

The name of the experiment.

 required

Raises:

Type Description
Exception

If a directory with the same name already exists.
Source code in ada_verona/database/experiment_repository.py 
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
def initialize_new_experiment(self, experiment_name: str) -> None:
    """
    Initialize a new experiment with the given name.

    Args:
        experiment_name (str): The name of the experiment.

    Raises:
        Exception: If a directory with the same name already exists.
    """
    now = datetime.now()
    now_string = now.strftime("%d-%m-%Y+%H_%M")

    self.act_experiment_path = self.base_path / f"{experiment_name}_{now_string}"

    if os.path.exists(self.get_results_path()):
        raise Exception(
            "Error, there is already a directory with results with the same name,"
            "make sure no results will be overwritten"  
        )
    else:
        os.makedirs(self.get_results_path())
    os.makedirs(self.get_tmp_path())

load_experiment(experiment_name)

Load an existing experiment with the given name.

Parameters:

Name Type Description Default
experiment_name str

The name of the experiment.

 required
Source code in ada_verona/database/experiment_repository.py 
110
111
112
113
114
115
116
117
def load_experiment(self, experiment_name: str) -> None:
    """
    Load an existing experiment with the given name.

    Args:
        experiment_name (str): The name of the experiment.
    """
    self.act_experiment_path = self.base_path / experiment_name

load_verification_context_from_yaml(file_path)

Load the verification context from a YAML file.

Parameters:

Name Type Description Default
file_path Path

The path to the YAML file.

 required

Returns:

Name Type Description
VerificationContext VerificationContext

The loaded verification context.
Source code in ada_verona/database/experiment_repository.py 
276
277
278
279
280
281
282
283
284
285
286
287
288
def load_verification_context_from_yaml(self, file_path: Path) -> VerificationContext:
    """
    Load the verification context from a YAML file.

    Args:
        file_path (Path): The path to the YAML file.

    Returns:
        VerificationContext: The loaded verification context.
    """
    with open(file_path) as file:
        data = yaml.safe_load(file)
        return VerificationContext.from_dict(data)

save_configuration(data)

Save the configuration data to a JSON file.

Parameters:

Name Type Description Default
data dict

The configuration data to save.

 required
Source code in ada_verona/database/experiment_repository.py 
119
120
121
122
123
124
125
126
127
def save_configuration(self, data: dict) -> None:
    """
    Save the configuration data to a JSON file.

    Args:
        data (dict): The configuration data to save.
    """
    with open(self.get_act_experiment_path() / "configuration.json", "w") as outfile:
        json.dump(data, outfile)

save_per_epsilon_result_df()

Save the per-epsilon result DataFrame to a CSV file.

Source code in ada_verona/database/experiment_repository.py 
236
237
238
239
240
241
def save_per_epsilon_result_df(self) -> None:
    """
    Save the per-epsilon result DataFrame to a CSV file.
    """
    per_epsilon_result_df = self.get_per_epsilon_result_df()
    per_epsilon_result_df.to_csv(self.get_results_path() / PER_EPSILON_RESULT_CSV_NAME)

save_plots()

Save the plots generated from the result DataFrame.

Source code in ada_verona/database/experiment_repository.py 
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
def save_plots(self) -> None:
    """
    Save the plots generated from the result DataFrame.
    """
    df = self.get_result_df()
    report_creator = ReportCreator(df)
    hist_figure = report_creator.create_hist_figure()
    hist_figure.savefig(self.get_results_path() / "hist_figure.png", bbox_inches="tight")

    boxplot = report_creator.create_box_figure()
    boxplot.savefig(self.get_results_path() / "boxplot.png", bbox_inches="tight")

    kde_figure = report_creator.create_kde_figure()
    kde_figure.savefig(self.get_results_path() / "kde_plot.png", bbox_inches="tight")

    ecdf_figure = report_creator.create_ecdf_figure()
    ecdf_figure.savefig(self.get_results_path() / "ecdf_plot.png", bbox_inches="tight")

save_result(result)

Save a single epsilon value result to the CSV file.

Parameters:

Name Type Description Default
result EpsilonValueResult

The epsilon value result to save.

 required
Source code in ada_verona/database/experiment_repository.py 
154
155
156
157
158
159
160
161
162
163
164
165
166
167
def save_result(self, result: EpsilonValueResult) -> None:
    """
    Save a single epsilon value result to the CSV file.

    Args:
        result (EpsilonValueResult): The epsilon value result to save.
    """
    result_df_path = self.get_results_path() / DEFAULT_RESULT_CSV_NAME
    if result_df_path.exists():
        df = pd.read_csv(result_df_path, index_col=0)
        df.loc[len(df.index)] = result.to_dict()
    else:
        df = pd.DataFrame([result.to_dict()])
    df.to_csv(result_df_path)

save_results(results)

Save the list of epsilon value results to a CSV file.

Parameters:

Name Type Description Default
results list[EpsilonValueResult]

The list of epsilon value results to save.

 required
Source code in ada_verona/database/experiment_repository.py 
144
145
146
147
148
149
150
151
152
def save_results(self, results: list[EpsilonValueResult]) -> None:
    """
    Save the list of epsilon value results to a CSV file.

    Args:
        results (list[EpsilonValueResult]): The list of epsilon value results to save.
    """
    result_df = pd.DataFrame([x.to_dict() for x in results])
    result_df.to_csv(self.get_results_path() / DEFAULT_RESULT_CSV_NAME)

save_verification_context_to_yaml(file_path, verification_context)

Save the verification context to a YAML file.

Parameters:

Name Type Description Default
file_path Path

The path to save the YAML file.

 required
verification_context VerificationContext

The verification context to save.

 required

Returns:

Name Type Description
Path Path

The path to the saved YAML file.
Source code in ada_verona/database/experiment_repository.py 
261
262
263
264
265
266
267
268
269
270
271
272
273
274
def save_verification_context_to_yaml(self, file_path: Path, verification_context: VerificationContext) -> Path:
    """
    Save the verification context to a YAML file.

    Args:
        file_path (Path): The path to save the YAML file.
        verification_context (VerificationContext): The verification context to save.

    Returns:
        Path: The path to the saved YAML file.
    """
    with open(file_path, "w") as file:
        yaml.dump(verification_context.to_dict(), file)
    return file_path

IterativeEpsilonValueEstimator

Bases: EpsilonValueEstimator

A class to estimate the epsilon value using an iterative search with configurable direction.

Source code in ada_verona/epsilon_value_estimator/iterative_epsilon_value_estimator.py 
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
class IterativeEpsilonValueEstimator(EpsilonValueEstimator):
    """
    A class to estimate the epsilon value using an iterative search with configurable direction.
    """
    def compute_epsilon_value(
    self,
    verification_context: VerificationContext,
    reverse_search=False,
) -> EpsilonValueResult:
        """
        Compute the epsilon value using an iterative search.

        Args:
            verification_context (VerificationContext): The context for verification.

        Returns:
            EpsilonValueResult: The result of the epsilon value estimation.
        """
        sorted_epsilons = sorted(self.epsilon_value_list, reverse=reverse_search)
        epsilon_status_list = [EpsilonStatus(x, None, None, self.verifier.name) for x in sorted_epsilons]
        start_time = time.time()
        highest_unsat_value, lowest_sat_value, epsilon_status_list = self.iterative_search(
            verification_context, epsilon_status_list
        )
        duration = time.time() - start_time
        epsilon_value_result = EpsilonValueResult(verification_context, 
                                                  highest_unsat_value, 
                                                  lowest_sat_value, 
                                                  duration, 
                                                  self.verifier.name)

        return epsilon_value_result

    def iterative_search(self, 
                         verification_context: VerificationContext, 
                        epsilon_status_list: list[EpsilonStatus]) -> tuple[float, float, list]:
        """
        Perform search and determine results based on actual epsilon values. 
        Find the highest UNSAT and smallest SAT epsilon values.

        Args:
            verification_context (VerificationContext): The context for verification.
            epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

        Returns:
            float: The highest UNSAT epsilon value.
            float: The smallest SAT epsilon value.
            list: The epsilon status list.
        """

        for status in epsilon_status_list:
            outcome = self.verifier.verify(verification_context, status.value)
            status.set_values(outcome)
            verification_context.save_result(status)
            logger.info(f"epsilon value: {status.value}, result: {status.result}")

        unsat_values = [x.value for x in epsilon_status_list if x.result == VerificationResult.UNSAT]
        sat_values = [x.value for x in epsilon_status_list if x.result == VerificationResult.SAT]

        highest_unsat = max(unsat_values) if unsat_values else 0
        lowest_sat = min(sat_values) if sat_values else 'undefined'


        return highest_unsat, lowest_sat, epsilon_status_list

compute_epsilon_value(verification_context, reverse_search=False)

Compute the epsilon value using an iterative search.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification.

 required

Returns:

Name Type Description
EpsilonValueResult EpsilonValueResult

The result of the epsilon value estimation.
Source code in ada_verona/epsilon_value_estimator/iterative_epsilon_value_estimator.py 
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
    def compute_epsilon_value(
    self,
    verification_context: VerificationContext,
    reverse_search=False,
) -> EpsilonValueResult:
        """
        Compute the epsilon value using an iterative search.

        Args:
            verification_context (VerificationContext): The context for verification.

        Returns:
            EpsilonValueResult: The result of the epsilon value estimation.
        """
        sorted_epsilons = sorted(self.epsilon_value_list, reverse=reverse_search)
        epsilon_status_list = [EpsilonStatus(x, None, None, self.verifier.name) for x in sorted_epsilons]
        start_time = time.time()
        highest_unsat_value, lowest_sat_value, epsilon_status_list = self.iterative_search(
            verification_context, epsilon_status_list
        )
        duration = time.time() - start_time
        epsilon_value_result = EpsilonValueResult(verification_context, 
                                                  highest_unsat_value, 
                                                  lowest_sat_value, 
                                                  duration, 
                                                  self.verifier.name)

        return epsilon_value_result

Perform search and determine results based on actual epsilon values. Find the highest UNSAT and smallest SAT epsilon values.

Parameters:

Name Type Description Default
verification_context VerificationContext

The context for verification.

 required
epsilon_status_list list[EpsilonStatus]

The list of epsilon statuses.

 required

Returns:

Name Type Description
float float

The highest UNSAT epsilon value.
float float

The smallest SAT epsilon value.
list list

The epsilon status list.
Source code in ada_verona/epsilon_value_estimator/iterative_epsilon_value_estimator.py 
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
def iterative_search(self, 
                     verification_context: VerificationContext, 
                    epsilon_status_list: list[EpsilonStatus]) -> tuple[float, float, list]:
    """
    Perform search and determine results based on actual epsilon values. 
    Find the highest UNSAT and smallest SAT epsilon values.

    Args:
        verification_context (VerificationContext): The context for verification.
        epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses.

    Returns:
        float: The highest UNSAT epsilon value.
        float: The smallest SAT epsilon value.
        list: The epsilon status list.
    """

    for status in epsilon_status_list:
        outcome = self.verifier.verify(verification_context, status.value)
        status.set_values(outcome)
        verification_context.save_result(status)
        logger.info(f"epsilon value: {status.value}, result: {status.result}")

    unsat_values = [x.value for x in epsilon_status_list if x.result == VerificationResult.UNSAT]
    sat_values = [x.value for x in epsilon_status_list if x.result == VerificationResult.SAT]

    highest_unsat = max(unsat_values) if unsat_values else 0
    lowest_sat = min(sat_values) if sat_values else 'undefined'


    return highest_unsat, lowest_sat, epsilon_status_list

Network

Bases: ABC

Abstract base class for networks that can be either ONNX or PyTorch.

This class provides a common interface for both network types.

Source code in ada_verona/database/machine_learning_model/network.py 
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
class Network(ABC):
    """
    Abstract base class for networks that can be either ONNX or PyTorch.

    This class provides a common interface for both network types.
    """

    @abstractmethod
    def load_pytorch_model(self) -> torch.nn.Module:
        """
        Load the PyTorch model.

        Returns:
            torch.nn.Module: The loaded PyTorch model.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")



    @abstractmethod
    def get_input_shape(self) -> np.ndarray | tuple[int, ...]:
        """
        Get the input shape of the model.

        Returns:
            Union[np.ndarray, tuple[int, ...]]: The input shape of the model.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")



    @abstractmethod
    def to_dict(self) -> dict:
        """
        Convert the network to a dictionary.

        Returns:
            dict: The dictionary representation of the network.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")



    @classmethod
    @abstractmethod
    def from_dict(cls, data: dict) -> "Network":
        """
        Create a network from a dictionary.

        Args:
            data (dict): The dictionary containing the network attributes.

        Returns:
            BaseNetwork: The created network.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")


    @property
    @abstractmethod
    def name(self) -> str:
        """
        Get the name of the network.

        Returns:
            str: The name of the network.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

    @property
    @abstractmethod
    def path(self) -> Path:
        """
        Get the path of the network.

        Returns:
            Path: The path of the network.
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

    @classmethod
    def from_file(cls, file: dict[Path]):
        """Create network from file
        Args: 
            file (dict[Path]): contains the paths to the relevant weights (for ONNX) 
            and additionally to the architecture file for PyTorch networks.

        Returns: 
            Created network from the correct class OR error. 
        """
        raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

name abstractmethod property

Get the name of the network.

Returns:

Name Type Description
str str

The name of the network.

path abstractmethod property

Get the path of the network.

Returns:

Name Type Description
Path Path

The path of the network.

from_dict(data) abstractmethod classmethod

Create a network from a dictionary.

Parameters:

Name Type Description Default
data dict

The dictionary containing the network attributes.

 required

Returns:

Name Type Description
BaseNetwork Network

The created network.
Source code in ada_verona/database/machine_learning_model/network.py 
66
67
68
69
70
71
72
73
74
75
76
77
78
@classmethod
@abstractmethod
def from_dict(cls, data: dict) -> "Network":
    """
    Create a network from a dictionary.

    Args:
        data (dict): The dictionary containing the network attributes.

    Returns:
        BaseNetwork: The created network.
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

from_file(file) classmethod

Create network from file Args: file (dict[Path]): contains the paths to the relevant weights (for ONNX) and additionally to the architecture file for PyTorch networks.

Returns:

Type Description

Created network from the correct class OR error.
Source code in ada_verona/database/machine_learning_model/network.py 
103
104
105
106
107
108
109
110
111
112
113
@classmethod
def from_file(cls, file: dict[Path]):
    """Create network from file
    Args: 
        file (dict[Path]): contains the paths to the relevant weights (for ONNX) 
        and additionally to the architecture file for PyTorch networks.

    Returns: 
        Created network from the correct class OR error. 
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

get_input_shape() abstractmethod

Get the input shape of the model.

Returns:

Type Description
ndarray | tuple[int, ...]

Union[np.ndarray, tuple[int, ...]]: The input shape of the model.
Source code in ada_verona/database/machine_learning_model/network.py 
42
43
44
45
46
47
48
49
50
@abstractmethod
def get_input_shape(self) -> np.ndarray | tuple[int, ...]:
    """
    Get the input shape of the model.

    Returns:
        Union[np.ndarray, tuple[int, ...]]: The input shape of the model.
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

load_pytorch_model() abstractmethod

Load the PyTorch model.

Returns:

Type Description
Module

torch.nn.Module: The loaded PyTorch model.
Source code in ada_verona/database/machine_learning_model/network.py 
30
31
32
33
34
35
36
37
38
@abstractmethod
def load_pytorch_model(self) -> torch.nn.Module:
    """
    Load the PyTorch model.

    Returns:
        torch.nn.Module: The loaded PyTorch model.
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

to_dict() abstractmethod

Convert the network to a dictionary.

Returns:

Name Type Description
dict dict

The dictionary representation of the network.
Source code in ada_verona/database/machine_learning_model/network.py 
54
55
56
57
58
59
60
61
62
@abstractmethod
def to_dict(self) -> dict:
    """
    Convert the network to a dictionary.

    Returns:
        dict: The dictionary representation of the network.
    """
    raise NotImplementedError("This is an abstract method and should be implemented in subclasses.")

ONNXNetwork

Bases: Network

Data class representing an ONNX network with its path.

Attributes:

Name Type Description
path Path

The path to the network file.
onnx_model ModelProto

The loaded ONNX model. Defaults to None.
torch_model_wrapper TorchModelWrapper

The PyTorch model wrapper. Defaults to None.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
class ONNXNetwork(Network):
    """
    Data class representing an ONNX network with its path.

    Attributes:
        path (Path): The path to the network file.
        onnx_model (onnx.ModelProto, optional): The loaded ONNX model. Defaults to None.
        torch_model_wrapper (TorchModelWrapper, optional): The PyTorch model wrapper. Defaults to None.
    """

    def __init__(self, path: Path) -> None:
        """
        Initialize the Network with the given path.

        Args:
            path (Path): The path to the network file.
        """
        self._path = path
        self.onnx_model = None
        self.torch_model_wrapper = None

    @property
    def name(self) -> str:
        """
        Get the name of the network.

        Returns:
            str: The name of the network.
        """
        return self.path.stem

    @property
    def path(self) -> Path:
        """
        Get the path of the network.

        Returns:
            Path: The path of the network.
        """
        return self._path

    def load_onnx_model(self) -> onnx.ModelProto:
        """
        Load the ONNX model from the network path.

        Returns:
            onnx.ModelProto: The loaded ONNX model.
        """
        model = self.onnx_model
        if model is None:
            model = onnx.load(str(self.path))
            self.onnx_model = model

        return model

    def get_input_shape(self) -> np.ndarray:
        """
        Get the input shape of the ONNX model.

        Returns:
            np.ndarray: The input shape of the ONNX model.
        """
        model = self.load_onnx_model()
        input_shape = tuple([d.dim_value for d in model.graph.input[0].type.tensor_type.shape.dim])
        input_shape = [x if x != 0 else -1 for x in input_shape]

        return input_shape

    def load_pytorch_model(self) -> torch.nn.Module:
        """
        Load the PyTorch model from the ONNX model.

        Returns:
            torch.nn.Module: The loaded PyTorch model.
        """
        device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
        torch_model_wrapper = self.torch_model_wrapper
        if torch_model_wrapper is None:
            torch_model = convert(self.path).to(device)
            torch_model_wrapper = TorchModelWrapper(torch_model, self.get_input_shape())
            self.torch_model_wrapper = torch_model_wrapper

        return torch_model_wrapper

    def to_dict(self) -> dict:
        """
        Convert the Network to a dictionary.

        Returns:
            dict: The dictionary representation of the Network.
        """

        return dict(network_path =  str(self.path), 
                type=self.__class__.__name__,
                module=self.__class__.__module__,
                    )

    @classmethod
    def from_dict(cls, data: dict)-> "ONNXNetwork":
        """
        Create a Network from a dictionary.

        Args:
            data (dict): The dictionary containing the Network attributes.

        Returns:
            Network: The created Network.
        """
        return cls(path = data['network_path'])

    @classmethod
    def from_file(cls, file:Path)-> "ONNXNetwork":
        """
        Create a ONNXNetwork from a dictionary.

        Args:
            file (Path): Path at which the network is stored. 

        Returns:
            ONNXNetwork: The created ONNXNetwork.
        """

        if not file.is_file():
            raise FileNotFoundError(f"File not found: {file}")

        return cls(path = file)

name property

Get the name of the network.

Returns:

Name Type Description
str str

The name of the network.

path property

Get the path of the network.

Returns:

Name Type Description
Path Path

The path of the network.

__init__(path)

Initialize the Network with the given path.

Parameters:

Name Type Description Default
path Path

The path to the network file.

 required
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
37
38
39
40
41
42
43
44
45
46
def __init__(self, path: Path) -> None:
    """
    Initialize the Network with the given path.

    Args:
        path (Path): The path to the network file.
    """
    self._path = path
    self.onnx_model = None
    self.torch_model_wrapper = None

from_dict(data) classmethod

Create a Network from a dictionary.

Parameters:

Name Type Description Default
data dict

The dictionary containing the Network attributes.

 required

Returns:

Name Type Description
Network ONNXNetwork

The created Network.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
124
125
126
127
128
129
130
131
132
133
134
135
@classmethod
def from_dict(cls, data: dict)-> "ONNXNetwork":
    """
    Create a Network from a dictionary.

    Args:
        data (dict): The dictionary containing the Network attributes.

    Returns:
        Network: The created Network.
    """
    return cls(path = data['network_path'])

from_file(file) classmethod

Create a ONNXNetwork from a dictionary.

Parameters:

Name Type Description Default
file Path

Path at which the network is stored.

required

Returns:

Name Type Description
ONNXNetwork ONNXNetwork

The created ONNXNetwork.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
@classmethod
def from_file(cls, file:Path)-> "ONNXNetwork":
    """
    Create a ONNXNetwork from a dictionary.

    Args:
        file (Path): Path at which the network is stored. 

    Returns:
        ONNXNetwork: The created ONNXNetwork.
    """

    if not file.is_file():
        raise FileNotFoundError(f"File not found: {file}")

    return cls(path = file)

get_input_shape()

Get the input shape of the ONNX model.

Returns:

Type Description
ndarray

np.ndarray: The input shape of the ONNX model.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
82
83
84
85
86
87
88
89
90
91
92
93
def get_input_shape(self) -> np.ndarray:
    """
    Get the input shape of the ONNX model.

    Returns:
        np.ndarray: The input shape of the ONNX model.
    """
    model = self.load_onnx_model()
    input_shape = tuple([d.dim_value for d in model.graph.input[0].type.tensor_type.shape.dim])
    input_shape = [x if x != 0 else -1 for x in input_shape]

    return input_shape

load_onnx_model()

Load the ONNX model from the network path.

Returns:

Type Description
ModelProto

onnx.ModelProto: The loaded ONNX model.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
68
69
70
71
72
73
74
75
76
77
78
79
80
def load_onnx_model(self) -> onnx.ModelProto:
    """
    Load the ONNX model from the network path.

    Returns:
        onnx.ModelProto: The loaded ONNX model.
    """
    model = self.onnx_model
    if model is None:
        model = onnx.load(str(self.path))
        self.onnx_model = model

    return model

load_pytorch_model()

Load the PyTorch model from the ONNX model.

Returns:

Type Description
Module

torch.nn.Module: The loaded PyTorch model.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
def load_pytorch_model(self) -> torch.nn.Module:
    """
    Load the PyTorch model from the ONNX model.

    Returns:
        torch.nn.Module: The loaded PyTorch model.
    """
    device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
    torch_model_wrapper = self.torch_model_wrapper
    if torch_model_wrapper is None:
        torch_model = convert(self.path).to(device)
        torch_model_wrapper = TorchModelWrapper(torch_model, self.get_input_shape())
        self.torch_model_wrapper = torch_model_wrapper

    return torch_model_wrapper

to_dict()

Convert the Network to a dictionary.

Returns:

Name Type Description
dict dict

The dictionary representation of the Network.
Source code in ada_verona/database/machine_learning_model/onnx_network.py 
111
112
113
114
115
116
117
118
119
120
121
122
def to_dict(self) -> dict:
    """
    Convert the Network to a dictionary.

    Returns:
        dict: The dictionary representation of the Network.
    """

    return dict(network_path =  str(self.path), 
            type=self.__class__.__name__,
            module=self.__class__.__module__,
                )

PyTorchNetwork

Bases: Network

A class representing a PyTorch network with architecture and weights files.

Attributes:

Name Type Description
model Module

The loaded PyTorch model. Defaults to None.
torch_model_wrapper TorchModelWrapper

The PyTorch model wrapper. Defaults to None.
name str

A chosen name for the model.
input_shape tuple[int]

Input shape of the model.
Source code in ada_verona/database/machine_learning_model/pytorch_network.py 
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
class PyTorchNetwork(Network):
    """
    A class representing a PyTorch network with architecture and weights files.

    Attributes:
        model (torch.nn.Module, optional): The loaded PyTorch model. Defaults to None.
        torch_model_wrapper (TorchModelWrapper, optional): The PyTorch model wrapper. Defaults to None.
        name: A chosen name for the model.
        input_shape (tuple[int]): Input shape of the model.
    """

    def __init__(self, model: torch.nn.Module, input_shape: tuple[int], name: str) -> None:
        """
        Initialize the PyTorchNetwork with architecture and weights paths.

        Args:
            model (torch.nn.Module, optional): The loaded PyTorch model. Defaults to None.
            input_shape (tuple[int]): Input shape of the model.
            name: A chosen name for the model.
        """

        self.model = model
        self.input_shape = input_shape
        self._name = name
        self.torch_model_wrapper = None

    @property
    def name(self) -> str:
        """
        Get the name of the network.

        Returns:
            str: The name of the network.
        """
        return self._name

    @property
    def path(self) -> Path:
        """
        Get the path of the network.

        Returns:
            Path: The path of the network.
        """
        return None

    def get_input_shape(self) -> np.ndarray:
        """
        Get the input shape of the PyTorch model.

        Returns:
            np.ndarray: the input_shape
        """

        return self.input_shape

    def load_pytorch_model(self) -> torch.nn.Module:
        """
        Load the PyTorch model and wrap it in a TorchModelWrapper.

        Returns:
            torch.nn.Module: The wrapped PyTorch model.
        """
        if self.torch_model_wrapper is None:
            device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
            model = self.model.to(device)
            model.eval()

            self.torch_model_wrapper = TorchModelWrapper(model, self.get_input_shape())

        return self.torch_model_wrapper


    def to_dict(self):
        raise NotImplementedError("PytorchNetwork does not support to_dict() function currently.")

    def from_dict(cls, data: dict):
         raise NotImplementedError("PytorchNetwork does not support from_dict() function currently.")

name property

Get the name of the network.

Returns:

Name Type Description
str str

The name of the network.

path property

Get the path of the network.

Returns:

Name Type Description
Path Path

The path of the network.

__init__(model, input_shape, name)

Initialize the PyTorchNetwork with architecture and weights paths.

Parameters:

Name Type Description Default
model Module

The loaded PyTorch model. Defaults to None.

 required
input_shape tuple[int]

Input shape of the model.

 required
name str

A chosen name for the model.

 required
Source code in ada_verona/database/machine_learning_model/pytorch_network.py 
36
37
38
39
40
41
42
43
44
45
46
47
48
49
def __init__(self, model: torch.nn.Module, input_shape: tuple[int], name: str) -> None:
    """
    Initialize the PyTorchNetwork with architecture and weights paths.

    Args:
        model (torch.nn.Module, optional): The loaded PyTorch model. Defaults to None.
        input_shape (tuple[int]): Input shape of the model.
        name: A chosen name for the model.
    """

    self.model = model
    self.input_shape = input_shape
    self._name = name
    self.torch_model_wrapper = None

get_input_shape()

Get the input shape of the PyTorch model.

Returns:

Type Description
ndarray

np.ndarray: the input_shape
Source code in ada_verona/database/machine_learning_model/pytorch_network.py 
71
72
73
74
75
76
77
78
79
def get_input_shape(self) -> np.ndarray:
    """
    Get the input shape of the PyTorch model.

    Returns:
        np.ndarray: the input_shape
    """

    return self.input_shape

load_pytorch_model()

Load the PyTorch model and wrap it in a TorchModelWrapper.

Returns:

Type Description
Module

torch.nn.Module: The wrapped PyTorch model.
Source code in ada_verona/database/machine_learning_model/pytorch_network.py 
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
def load_pytorch_model(self) -> torch.nn.Module:
    """
    Load the PyTorch model and wrap it in a TorchModelWrapper.

    Returns:
        torch.nn.Module: The wrapped PyTorch model.
    """
    if self.torch_model_wrapper is None:
        device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
        model = self.model.to(device)
        model.eval()

        self.torch_model_wrapper = TorchModelWrapper(model, self.get_input_shape())

    return self.torch_model_wrapper

TorchModelWrapper

Bases: Module

A wrapper class for a PyTorch model to reshape the input before passing it to the model.

Source code in ada_verona/database/machine_learning_model/torch_model_wrapper.py 
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
class TorchModelWrapper(torch.nn.Module):
    """
    A wrapper class for a PyTorch model to reshape the input before passing it to the model.
    """

    def __init__(self, torch_model: torch.nn.Module, input_shape: tuple[int]):
        """
        Initialize the TorchModelWrapper with the given PyTorch model and input shape.

        Args:
            torch_model (torch.nn.Module): The PyTorch model to wrap.
            input_shape: The input shape to reshape the input tensor. Can be tuple[int] or np.ndarray.
        """
        super().__init__()
        self.torch_model = torch_model
        self.input_shape = input_shape

    def forward(self, x):
        """
        Forward pass of the TorchModelWrapper.

        Args:
            x (torch.Tensor): The input tensor.

        Returns:
            torch.Tensor: The output tensor from the wrapped PyTorch model.
        """

        if isinstance(x, np.ndarray):
        # ensure correct dtype/device if needed
            x = torch.from_numpy(x).to(
                dtype=torch.float32,
                device=next(self.torch_model.parameters()).device
            )
            x = x.reshape(*self.input_shape)  # tuple unpacking

        else:
        # Assume it's already a torch.Tensor
            x = x.reshape(*self.input_shape)

        x = self.torch_model(x)
        return x

__init__(torch_model, input_shape)

Initialize the TorchModelWrapper with the given PyTorch model and input shape.

Parameters:

Name Type Description Default
torch_model Module

The PyTorch model to wrap.

 required
input_shape tuple[int]

The input shape to reshape the input tensor. Can be tuple[int] or np.ndarray.

 required
Source code in ada_verona/database/machine_learning_model/torch_model_wrapper.py 
25
26
27
28
29
30
31
32
33
34
35
def __init__(self, torch_model: torch.nn.Module, input_shape: tuple[int]):
    """
    Initialize the TorchModelWrapper with the given PyTorch model and input shape.

    Args:
        torch_model (torch.nn.Module): The PyTorch model to wrap.
        input_shape: The input shape to reshape the input tensor. Can be tuple[int] or np.ndarray.
    """
    super().__init__()
    self.torch_model = torch_model
    self.input_shape = input_shape

forward(x)

Forward pass of the TorchModelWrapper.

Parameters:

Name Type Description Default
x Tensor

The input tensor.

 required

Returns:

Type Description

torch.Tensor: The output tensor from the wrapped PyTorch model.
Source code in ada_verona/database/machine_learning_model/torch_model_wrapper.py 
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
def forward(self, x):
    """
    Forward pass of the TorchModelWrapper.

    Args:
        x (torch.Tensor): The input tensor.

    Returns:
        torch.Tensor: The output tensor from the wrapped PyTorch model.
    """

    if isinstance(x, np.ndarray):
    # ensure correct dtype/device if needed
        x = torch.from_numpy(x).to(
            dtype=torch.float32,
            device=next(self.torch_model.parameters()).device
        )
        x = x.reshape(*self.input_shape)  # tuple unpacking

    else:
    # Assume it's already a torch.Tensor
        x = x.reshape(*self.input_shape)

    x = self.torch_model(x)
    return x

VNNLibProperty dataclass

Dataclass for a VNNLib property.

Source code in ada_verona/database/vnnlib_property.py 
20
21
22
23
24
25
26
@dataclass
class VNNLibProperty:
    """Dataclass for a VNNLib property."""

    name: str
    content: str
    path: Path = None

VerificationContext

A class to represent the context for verification. This class saves all the relevant information for a verification run.

Source code in ada_verona/database/verification_context.py 
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
class VerificationContext:
    """
    A class to represent the context for verification.
    This class saves all the relevant information for a verification run.
    """

    def __init__(
        self,
        network: Network,
        data_point: DataPoint,
        tmp_path: Path,
        property_generator: PropertyGenerator,
        save_epsilon_results: bool = True,
    ) -> None:
        """
        Initialize the VerificationContext with the given parameters.

        Args:
            network (Network): The network to be verified.
            data_point (DataPoint): The data point to be verified.
            tmp_path (Path): The temporary path for saving intermediate results.
            property_generator (PropertyGenerator): The property generator for creating verification properties.
            save_epsilon_results (bool, optional): Whether to save epsilon results. Defaults to True.
        """
        self.network = network
        self.data_point = data_point
        self.tmp_path = tmp_path
        self.property_generator = property_generator
        self.save_epsilon_results = save_epsilon_results

        if save_epsilon_results and not self.tmp_path.exists():
            self.tmp_path.mkdir(parents=True)

    def get_dict_for_epsilon_result(self) -> dict:
        """
        Get a dictionary representation of the epsilon result.

        Returns:
            dict: The dictionary representation of the epsilon result.
        """
        return dict(
            network=self.network.name,
            image_id=self.data_point.id,
            original_label=self.data_point.label,
            tmp_path=self.tmp_path.resolve(),
            **self.property_generator.get_dict_for_epsilon_result(),
        )

    def save_vnnlib_property(self, vnnlib_property: VNNLibProperty) -> None:
        """
        Save the VNNLib property to a file in the temporary path.

        Args:
            vnnlib_property (VNNLibProperty): The VNNLib property object to be saved.
        """
        if not self.tmp_path.exists():
            self.tmp_path.mkdir(parents=True)
        save_path = self.tmp_path / f"{vnnlib_property.name}.vnnlib"

        with open(save_path, "w") as f:
            f.write(vnnlib_property.content)
        vnnlib_property.path = save_path

    def delete_tmp_path(self) -> None:
        """
        Delete the temporary path and its contents.
        """


        self.tmp_path.unlink()


    def save_status_list(self, epsilon_status_list: list[EpsilonStatus]) -> None:
        """
        Save the list of epsilon statuses to a CSV file.

        Args:
            epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses to save.
        """
        save_path = self.tmp_path / "epsilon_results.csv"
        data = [x.to_dict() for x in epsilon_status_list]
        df = pd.DataFrame(data=data)
        df.to_csv(save_path)

    def save_result(self, result: EpsilonStatus) -> None:
        """
        Save a single epsilon status result to the CSV file.

        Args:
            result (EpsilonStatus): The epsilon status result to save.
        """
        if self.save_epsilon_results:
            result_df_path = self.tmp_path / "epsilons_df.csv"
            if result_df_path.exists():
                df = pd.read_csv(result_df_path, index_col=0)
                df.loc[len(df.index)] = result.to_dict()
            else:
                df = pd.DataFrame([result.to_dict()])
            df.to_csv(result_df_path)

    def to_dict(self) -> dict:
        """
        Convert the VerificationContext to a dictionary.

        Returns:
            dict: The dictionary representation of the VerificationContext.
        """
        return {
            "network": self.network.to_dict(),
            "data_point": self.data_point.to_dict(),
            "tmp_path": str(self.tmp_path),
            "property_generator": self.property_generator.to_dict(),
            "save_epsilon_results": self.save_epsilon_results,
        }

    @classmethod
    def from_dict(cls, data: dict) -> "VerificationContext":
        """
        Create a VerificationContext from a dictionary.

        Args:
            data (dict): The dictionary containing the VerificationContext attributes.

        Returns:
            VerificationContext: The created VerificationContext.
        """
        # Recreate the network from its dictionary representation

        network = ONNXNetwork.from_dict(data["network"]) 
        data_point = DataPoint.from_dict(data["data_point"])
        tmp_path = Path(data["tmp_path"])
        property_generator = PropertyGenerator.from_dict(data["property_generator"])
        save_epsilon_results = data["save_epsilon_results"]
        return cls(
            network=network,
            data_point=data_point,
            tmp_path=tmp_path,
            property_generator=property_generator,
            save_epsilon_results=save_epsilon_results,
        )

__init__(network, data_point, tmp_path, property_generator, save_epsilon_results=True)

Initialize the VerificationContext with the given parameters.

Parameters:

Name Type Description Default
network Network

The network to be verified.

 required
data_point DataPoint

The data point to be verified.

 required
tmp_path Path

The temporary path for saving intermediate results.

 required
property_generator PropertyGenerator

The property generator for creating verification properties.

 required
save_epsilon_results bool

Whether to save epsilon results. Defaults to True.

 True
Source code in ada_verona/database/verification_context.py 
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
def __init__(
    self,
    network: Network,
    data_point: DataPoint,
    tmp_path: Path,
    property_generator: PropertyGenerator,
    save_epsilon_results: bool = True,
) -> None:
    """
    Initialize the VerificationContext with the given parameters.

    Args:
        network (Network): The network to be verified.
        data_point (DataPoint): The data point to be verified.
        tmp_path (Path): The temporary path for saving intermediate results.
        property_generator (PropertyGenerator): The property generator for creating verification properties.
        save_epsilon_results (bool, optional): Whether to save epsilon results. Defaults to True.
    """
    self.network = network
    self.data_point = data_point
    self.tmp_path = tmp_path
    self.property_generator = property_generator
    self.save_epsilon_results = save_epsilon_results

    if save_epsilon_results and not self.tmp_path.exists():
        self.tmp_path.mkdir(parents=True)

delete_tmp_path()

Delete the temporary path and its contents.

Source code in ada_verona/database/verification_context.py 
91
92
93
94
95
96
97
def delete_tmp_path(self) -> None:
    """
    Delete the temporary path and its contents.
    """


    self.tmp_path.unlink()

from_dict(data) classmethod

Create a VerificationContext from a dictionary.

Parameters:

Name Type Description Default
data dict

The dictionary containing the VerificationContext attributes.

 required

Returns:

Name Type Description
VerificationContext VerificationContext

The created VerificationContext.
Source code in ada_verona/database/verification_context.py 
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
@classmethod
def from_dict(cls, data: dict) -> "VerificationContext":
    """
    Create a VerificationContext from a dictionary.

    Args:
        data (dict): The dictionary containing the VerificationContext attributes.

    Returns:
        VerificationContext: The created VerificationContext.
    """
    # Recreate the network from its dictionary representation

    network = ONNXNetwork.from_dict(data["network"]) 
    data_point = DataPoint.from_dict(data["data_point"])
    tmp_path = Path(data["tmp_path"])
    property_generator = PropertyGenerator.from_dict(data["property_generator"])
    save_epsilon_results = data["save_epsilon_results"]
    return cls(
        network=network,
        data_point=data_point,
        tmp_path=tmp_path,
        property_generator=property_generator,
        save_epsilon_results=save_epsilon_results,
    )

get_dict_for_epsilon_result()

Get a dictionary representation of the epsilon result.

Returns:

Name Type Description
dict dict

The dictionary representation of the epsilon result.
Source code in ada_verona/database/verification_context.py 
61
62
63
64
65
66
67
68
69
70
71
72
73
74
def get_dict_for_epsilon_result(self) -> dict:
    """
    Get a dictionary representation of the epsilon result.

    Returns:
        dict: The dictionary representation of the epsilon result.
    """
    return dict(
        network=self.network.name,
        image_id=self.data_point.id,
        original_label=self.data_point.label,
        tmp_path=self.tmp_path.resolve(),
        **self.property_generator.get_dict_for_epsilon_result(),
    )

save_result(result)

Save a single epsilon status result to the CSV file.

Parameters:

Name Type Description Default
result EpsilonStatus

The epsilon status result to save.

 required
Source code in ada_verona/database/verification_context.py 
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
def save_result(self, result: EpsilonStatus) -> None:
    """
    Save a single epsilon status result to the CSV file.

    Args:
        result (EpsilonStatus): The epsilon status result to save.
    """
    if self.save_epsilon_results:
        result_df_path = self.tmp_path / "epsilons_df.csv"
        if result_df_path.exists():
            df = pd.read_csv(result_df_path, index_col=0)
            df.loc[len(df.index)] = result.to_dict()
        else:
            df = pd.DataFrame([result.to_dict()])
        df.to_csv(result_df_path)

save_status_list(epsilon_status_list)

Save the list of epsilon statuses to a CSV file.

Parameters:

Name Type Description Default
epsilon_status_list list[EpsilonStatus]

The list of epsilon statuses to save.

 required
Source code in ada_verona/database/verification_context.py 
100
101
102
103
104
105
106
107
108
109
110
def save_status_list(self, epsilon_status_list: list[EpsilonStatus]) -> None:
    """
    Save the list of epsilon statuses to a CSV file.

    Args:
        epsilon_status_list (list[EpsilonStatus]): The list of epsilon statuses to save.
    """
    save_path = self.tmp_path / "epsilon_results.csv"
    data = [x.to_dict() for x in epsilon_status_list]
    df = pd.DataFrame(data=data)
    df.to_csv(save_path)

save_vnnlib_property(vnnlib_property)

Save the VNNLib property to a file in the temporary path.

Parameters:

Name Type Description Default
vnnlib_property VNNLibProperty

The VNNLib property object to be saved.

 required
Source code in ada_verona/database/verification_context.py 
76
77
78
79
80
81
82
83
84
85
86
87
88
89
def save_vnnlib_property(self, vnnlib_property: VNNLibProperty) -> None:
    """
    Save the VNNLib property to a file in the temporary path.

    Args:
        vnnlib_property (VNNLibProperty): The VNNLib property object to be saved.
    """
    if not self.tmp_path.exists():
        self.tmp_path.mkdir(parents=True)
    save_path = self.tmp_path / f"{vnnlib_property.name}.vnnlib"

    with open(save_path, "w") as f:
        f.write(vnnlib_property.content)
    vnnlib_property.path = save_path

to_dict()

Convert the VerificationContext to a dictionary.

Returns:

Name Type Description
dict dict

The dictionary representation of the VerificationContext.
Source code in ada_verona/database/verification_context.py 
128
129
130
131
132
133
134
135
136
137
138
139
140
141
def to_dict(self) -> dict:
    """
    Convert the VerificationContext to a dictionary.

    Returns:
        dict: The dictionary representation of the VerificationContext.
    """
    return {
        "network": self.network.to_dict(),
        "data_point": self.data_point.to_dict(),
        "tmp_path": str(self.tmp_path),
        "property_generator": self.property_generator.to_dict(),
        "save_epsilon_results": self.save_epsilon_results,
    }

VerificationModule

Bases: ABC

Source code in ada_verona/verification_module/verification_module.py 
22
23
24
25
26
class VerificationModule(ABC):
    @abstractmethod
    def verify(self, verification_context: VerificationContext, epsilon: float) -> str | CompleteVerificationData:
        """Main method to verify an image for a given network and epsilon value"""
        raise NotImplementedError

verify(verification_context, epsilon) abstractmethod

Main method to verify an image for a given network and epsilon value

Source code in ada_verona/verification_module/verification_module.py 
23
24
25
26
@abstractmethod
def verify(self, verification_context: VerificationContext, epsilon: float) -> str | CompleteVerificationData:
    """Main method to verify an image for a given network and epsilon value"""
    raise NotImplementedError

VerificationResult

Bases: str, Enum

Class for saving the possible verification results. At this point we are using the same Result strings for complete verification and attacks.

Source code in ada_verona/database/verification_result.py 
23
24
25
26
27
28
29
30
31
class VerificationResult(str, Enum):
    """Class for saving the possible verification results.
    At this point we are using the same Result strings for complete verification and attacks.
    """

    UNSAT = "UNSAT"
    SAT = "SAT"
    TIMEOUT = "TIMEOUT"
    ERROR = "ERR"