Delete phis_generator.py
Browse files- phis_generator.py +0 -157
phis_generator.py
DELETED
|
@@ -1,157 +0,0 @@
|
|
| 1 |
-
import stl
|
| 2 |
-
import numpy.random as rnd
|
| 3 |
-
from typing import Union
|
| 4 |
-
from stl import Node
|
| 5 |
-
|
| 6 |
-
|
| 7 |
-
class StlGenerator:
|
| 8 |
-
def __init__(
|
| 9 |
-
self,
|
| 10 |
-
leaf_prob: float = 0.3,
|
| 11 |
-
inner_node_prob: list = None,
|
| 12 |
-
threshold_mean: float = 0.0,
|
| 13 |
-
threshold_sd: float = 1.0,
|
| 14 |
-
unbound_prob: float = 0.1,
|
| 15 |
-
right_unbound_prob: float = 0.2,
|
| 16 |
-
time_bound_max_range: float = 20,
|
| 17 |
-
adaptive_unbound_temporal_ops: bool = True,
|
| 18 |
-
max_timespan: int = 100,
|
| 19 |
-
):
|
| 20 |
-
"""
|
| 21 |
-
leaf_prob
|
| 22 |
-
probability of generating a leaf (always zero for root)
|
| 23 |
-
node_types = ["not", "and", "or", "always", "eventually", "until"]
|
| 24 |
-
Inner node types
|
| 25 |
-
inner_node_prob
|
| 26 |
-
probability vector for the different types of internal nodes
|
| 27 |
-
threshold_mean
|
| 28 |
-
threshold_sd
|
| 29 |
-
mean and std for the normal distribution of the thresholds of atoms
|
| 30 |
-
unbound_prob
|
| 31 |
-
probability of a temporal operator to have a time bound o the type [0,infty]
|
| 32 |
-
time_bound_max_range
|
| 33 |
-
maximum value of time span of a temporal operator (i.e. max value of t in [0,t])
|
| 34 |
-
adaptive_unbound_temporal_ops
|
| 35 |
-
if true, unbounded temporal operators are computed from current point to the end of the signal, otherwise
|
| 36 |
-
they are evaluated only at time zero.
|
| 37 |
-
max_timespan
|
| 38 |
-
maximum time depth of a formula.
|
| 39 |
-
"""
|
| 40 |
-
|
| 41 |
-
# Address the mutability of default arguments
|
| 42 |
-
if inner_node_prob is None:
|
| 43 |
-
inner_node_prob = [0.166, 0.166, 0.166, 0.17, 0.166, 0.166]
|
| 44 |
-
|
| 45 |
-
self.leaf_prob = leaf_prob
|
| 46 |
-
self.inner_node_prob = inner_node_prob
|
| 47 |
-
self.threshold_mean = threshold_mean
|
| 48 |
-
self.threshold_sd = threshold_sd
|
| 49 |
-
self.unbound_prob = unbound_prob
|
| 50 |
-
self.right_unbound_prob = right_unbound_prob
|
| 51 |
-
self.time_bound_max_range = time_bound_max_range
|
| 52 |
-
self.adaptive_unbound_temporal_ops = adaptive_unbound_temporal_ops
|
| 53 |
-
self.node_types = ["not", "and", "or", "always", "eventually", "until"]
|
| 54 |
-
self.max_timespan = max_timespan
|
| 55 |
-
|
| 56 |
-
def sample(self, nvars):
|
| 57 |
-
"""
|
| 58 |
-
Samples a random formula with distribution defined in class instance parameters
|
| 59 |
-
|
| 60 |
-
Parameters
|
| 61 |
-
----------
|
| 62 |
-
nvars : number of variables of input signals
|
| 63 |
-
how many variables the formula is expected to consider.
|
| 64 |
-
|
| 65 |
-
Returns
|
| 66 |
-
-------
|
| 67 |
-
TYPE
|
| 68 |
-
A random formula.
|
| 69 |
-
|
| 70 |
-
"""
|
| 71 |
-
return self._sample_internal_node(nvars)
|
| 72 |
-
|
| 73 |
-
def bag_sample(self, bag_size, nvars):
|
| 74 |
-
"""
|
| 75 |
-
Samples a bag of bag_size formulae
|
| 76 |
-
|
| 77 |
-
Parameters
|
| 78 |
-
----------
|
| 79 |
-
bag_size : INT
|
| 80 |
-
number of formulae.
|
| 81 |
-
nvars : INT
|
| 82 |
-
number of vars in formulae.
|
| 83 |
-
|
| 84 |
-
Returns
|
| 85 |
-
-------
|
| 86 |
-
a list of formulae.
|
| 87 |
-
|
| 88 |
-
"""
|
| 89 |
-
formulae = []
|
| 90 |
-
for _ in range(bag_size):
|
| 91 |
-
phi = self.sample(nvars)
|
| 92 |
-
formulae.append(phi)
|
| 93 |
-
return formulae
|
| 94 |
-
|
| 95 |
-
def _sample_internal_node(self, nvars):
|
| 96 |
-
# Declare & dummy-assign "idiom"
|
| 97 |
-
node: Union[None, Node]
|
| 98 |
-
node = None
|
| 99 |
-
# choose node type
|
| 100 |
-
nodetype = rnd.choice(self.node_types, p=self.inner_node_prob)
|
| 101 |
-
while True:
|
| 102 |
-
if nodetype == "not":
|
| 103 |
-
n = self._sample_node(nvars)
|
| 104 |
-
node = stl.Not(n)
|
| 105 |
-
elif nodetype == "and":
|
| 106 |
-
n1 = self._sample_node(nvars)
|
| 107 |
-
n2 = self._sample_node(nvars)
|
| 108 |
-
node = stl.And(n1, n2)
|
| 109 |
-
elif nodetype == "or":
|
| 110 |
-
n1 = self._sample_node(nvars)
|
| 111 |
-
n2 = self._sample_node(nvars)
|
| 112 |
-
node = stl.Or(n1, n2)
|
| 113 |
-
elif nodetype == "always":
|
| 114 |
-
n = self._sample_node(nvars)
|
| 115 |
-
unbound, right_unbound, left_time_bound, right_time_bound = self._get_temporal_parameters()
|
| 116 |
-
node = stl.Globally(
|
| 117 |
-
n, unbound, right_unbound, left_time_bound, right_time_bound, self.adaptive_unbound_temporal_ops
|
| 118 |
-
)
|
| 119 |
-
elif nodetype == "eventually":
|
| 120 |
-
n = self._sample_node(nvars)
|
| 121 |
-
unbound, right_unbound, left_time_bound, right_time_bound = self._get_temporal_parameters()
|
| 122 |
-
node = stl.Eventually(
|
| 123 |
-
n, unbound, right_unbound, left_time_bound, right_time_bound, self.adaptive_unbound_temporal_ops
|
| 124 |
-
)
|
| 125 |
-
elif nodetype == "until":
|
| 126 |
-
n1 = self._sample_node(nvars)
|
| 127 |
-
n2 = self._sample_node(nvars)
|
| 128 |
-
unbound, right_unbound, left_time_bound, right_time_bound = self._get_temporal_parameters()
|
| 129 |
-
node = stl.Until(
|
| 130 |
-
n1, n2, unbound, right_unbound, left_time_bound, right_time_bound
|
| 131 |
-
)
|
| 132 |
-
|
| 133 |
-
if (node is not None) and (node.time_depth() < self.max_timespan):
|
| 134 |
-
return node
|
| 135 |
-
|
| 136 |
-
def _sample_node(self, nvars):
|
| 137 |
-
if rnd.rand() < self.leaf_prob:
|
| 138 |
-
# sample a leaf
|
| 139 |
-
var, thr, lte = self._get_atom(nvars)
|
| 140 |
-
return stl.Atom(var, thr, lte)
|
| 141 |
-
else:
|
| 142 |
-
return self._sample_internal_node(nvars)
|
| 143 |
-
|
| 144 |
-
def _get_temporal_parameters(self):
|
| 145 |
-
if rnd.rand() < self.unbound_prob:
|
| 146 |
-
return True, False, 0, 0
|
| 147 |
-
elif rnd.rand() < self.right_unbound_prob:
|
| 148 |
-
return False, True, rnd.randint(self.time_bound_max_range), 1
|
| 149 |
-
else:
|
| 150 |
-
left_bound = rnd.randint(self.time_bound_max_range)
|
| 151 |
-
return False, False, left_bound, rnd.randint(left_bound, self.time_bound_max_range) + 1
|
| 152 |
-
|
| 153 |
-
def _get_atom(self, nvars):
|
| 154 |
-
variable = rnd.randint(nvars)
|
| 155 |
-
lte = rnd.rand() > 0.5
|
| 156 |
-
threshold = rnd.normal(self.threshold_mean, self.threshold_sd)
|
| 157 |
-
return variable, threshold, lte
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|