Actualize examples basic-1 and basic-2

Author: p-senichenkov

examples/basic/verifying_pac/verifying_domain_pac1.py

@@ -6,79 +6,128 @@
 import desbordante
 
 RED = '\033[31m'
+YELLOW = '\033[33m'
+BOLD_YELLOW = '\033[1;33m'
 GREEN = '\033[32m'
 BLUE = '\033[34m'
 CYAN = '\033[36m'
-GRAY = '\033[1;30m'
+BOLD = '\033[1;37m'
 ENDC = '\033[0m'
 
 ENGINE_TEMPS_BAD = 'examples/datasets/verifying_pac/engine_temps_bad.csv'
 ENGINE_TEMPS_GOOD = 'examples/datasets/verifying_pac/engine_temps_good.csv'
 
 
-def column_to_str(filename: str) -> str:
+def read_column(filename: str, col_num: int) -> (str, list[str]):
     with open(filename, newline='') as table:
         rows = list(reader(table, delimiter=','))
-    headers = rows[0]
-    rows = rows[1:]
-    values = ', '.join(list(map(lambda row: str(row[0]), rows)))
-    return f'{headers[0]}: [{values}]'
+    header = rows[0][col_num]
+    values = [row[col_num] for row in rows[1:]]
+    return header, values
+
+
+def column_to_str(filename: str, col_num: int) -> str:
+    header, values = read_column(filename, col_num)
+    values_str = ', '.join(values)
+    return f'{BOLD}{header}: [{values_str}]{ENDC}'
+
+
+def display_columns_diff(filename_old: str, col_num_old: int,
+                         filename_new: str, col_num_new: int) -> str:
+    _, values_old = read_column(filename_old, col_num_old)
+    header, values_new = read_column(filename_new, col_num_new)
+    values = []
+    for i in range(len(values_new)):
+        value = values_new[i]
+        if values_old[i] != value:
+            value = f'{BOLD_YELLOW}' + value + f'{BOLD}'
+        values.append(value)
+    values_str = ', '.join(values)
+    return f'{BOLD}{header}: [{values_str}]{ENDC}'
 
 
 print(
-    f'''{CYAN}This example illustrates the usage of Domain Probabilistic Approximate Constraints (PACs).
-Domain PAC on column set X and domain D, with given epsilon and delta means that Pr(x ∈ D±epsilon) ≥ delta.
+    f'''This example illustrates the usage of Domain Probabilistic Approximate Constraints (PACs).
+A Domain PAC on column set X and domain D, with given ε and δ means that Pr(x ∈ D±ε) ≥ δ.
 For more information consult "Checks and Balances: Monitoring Data Quality Problems in Network
-Traffic Databases" by Flip Korn et al.
+Traffic Databases" by Flip Korn et al (Proceedings of the 29th VLDB Conference, Berlin, 2003).
 
-This is the first example in "Basic Domain PAC verification" series. Others can be found in
-examples/basic/verifying_pac/{ENDC} directory.
+This is the first example in the "Basic Domain PAC verification" series. Others can be found in
+{CYAN}examples/basic/verifying_pac/{ENDC} directory.
 ''')
 
 print(
-    f'''Consider we are working on a new model of engine. It\'s working temperatures lie in span {BLUE}[85, 95]{ENDC}°C.
-Engine is made of high-strenght metal, so slight short-term temperature deviations won\'t kill it.
-In other words, engine works properly when Pr(t ∈ [85, 95]±epsilon) ≥ delta.
-Our engieneers have figured out limits: epsilon = {BLUE}5{ENDC}, delta = {BLUE}0.9{ENDC}.
-So, in terms of Domain PACs, {BLUE}Domain PAC Pr(x ∈ [85, 95]±5) ≥ 0.9{ENDC} should hold.
+    f'''Suppose we are working on a new model of engine. Its operating temperature range is {BLUE}[85, 95]{ENDC}°C.
+The engine is made of high-strength metal, so short-term temperature deviations are acceptable and
+will not cause immediate damage. In other words, engine operates properly when Pr(t ∈ [85, 95]±ε) ≥ δ.
+Based on enginnering analysis, the acceptable limits are: ε = {BLUE}5{ENDC}, δ = {BLUE}0.9{ENDC}.
+In terms of Domain PACs, the following constraint should hold: {BLUE}Pr(x ∈ [85, 95]±5) ≥ 0.9{ENDC}.
 ''')
 
-print('The following table contains readings of engine temperature sensor:')
+print(
+    'The following table contains readings from the engine temperature sensor:'
+)
 # Values are printed in one line for brevity, original table is single-column
-print(f'{GRAY}{column_to_str(ENGINE_TEMPS_BAD)}{ENDC}')
+print(f'{column_to_str(ENGINE_TEMPS_BAD, 0)}')
 print()
 
-print('Let\'s use Domain PAC verifier to check if engine will be damaged\n')
+print(
+    'We now use the Domain PAC verifier to determine whether the engine is operating safely.'
+)
 
 print(
-    'Firstly we need to create domain. Segment is a special case of parallelepiped, so let\'s use it.'
+    'First, we need to define the domain. A segment is a special case of a parallelepiped, so we use it here.'
 )
 # Parallelepiped has a special constructor for segment.
-# Notice the usage of quotes: these strings will be converted to values once table is loaded.
+# Notice the usage of quotes: these strings will be converted to values once the table is loaded.
 segment = desbordante.pac.domains.Parallelepiped('85', '95')
 
-# TODO(senichenkov): diagonal_threshold example
 print(
-    f'''Now let\'s run algorithm with the following options: domain={BLUE}{segment}{ENDC}, max_epsilon={BLUE}10{ENDC}, min_delta={BLUE}0.85{ENDC}.
-Max_epsilon should be greater than desired epsilon, min_delta -- a little less than the expected one.
-We will use default values of other options: min_epsilon={BLUE}0{ENDC}, epsilon_steps={BLUE}100{ENDC}, diagonal_threshold={BLUE}1e-5{ENDC}.
-Min_epsilon, max_epsilon and epsilon_steps contol which epsilon values and how many of them will be checked by the algorithm.
-Diagonal threshold is advanced parameter, that is explained in {CYAN}examples/advanced/verifying_pac/##EXAMPLE_NAME##{ENDC}.
+    f'''We run algorithm with the following options: domain={BLUE}{segment}{ENDC}.
+All other parameters use default values: min_epsilon={BLUE}0{ENDC}, max_epsilon={BLUE}∞{ENDC}, min_delta={BLUE}0.9{ENDC}, delta_steps={BLUE}100{ENDC}.
 ''')
+
 algo = desbordante.pac_verification.algorithms.DomainPACVerifier()
 # Note that domain should be set in `load_data`, not `execute`
 algo.load_data(table=(ENGINE_TEMPS_BAD, ',', True),
                column_indices=[0],
                domain=segment)
-algo.execute(max_epsilon=10, min_delta=0.85)
+algo.execute()
+
+print(f'Algorithm result: {YELLOW}{algo.get_pac()}{ENDC}.')
+print(
+    f'''This PAC is not very informative. Let\'s run algorithm with min_epsilon={BLUE}5{ENDC} and max_epsilon={BLUE}5{ENDC}.
+This will give us the exact δ, for which PAC with ε={BLUE}5{ENDC} holds.
+''')
+
+# Note that, when min_epsilon or max_epsilon is specified, default min_delta becomes 0
+algo.execute(min_epsilon=5, max_epsilon=5)
 
 print(f'Algorithm result: {RED}{algo.get_pac()}{ENDC}.')
-print('Uh-oh! The desired PAC doesn\'t hold, so engine can blow up!\n')
+print(
+    f'''Also, let\'s run algorithm with max_epsilon={BLUE}0{ENDC} and min_delta={BLUE}0.9{ENDC} to check which ε
+is needed to satisfy δ={BLUE}0.9{ENDC}. With these parameters algorithm enter special mode and returns
+pair (ε, min_delta), so that we can validate PAC with the given δ.
+''')
+
+# Actually, algorithm enter this mode whenever max_epsilon is less than epsislon needed to satisfy
+# min_delta.
+algo.execute(max_epsilon=0, min_delta=0.9)
+
+pac = algo.get_pac()
+print(f'Algorithm result: {RED}{pac}{ENDC}.')
+print(
+    f'''Here algorithm gives δ={BLUE}{pac.delta}{ENDC}, which is greater than {BLUE}0.9{ENDC}, because achieving δ={BLUE}0.9{ENDC} requires
+ε={BLUE}{pac.epsilon}{ENDC} and PAC ({BLUE}{pac.epsilon}{ENDC}, {BLUE}{pac.delta}{ENDC}) holds. So, this means that δ={BLUE}0.9{ENDC} would also require ε={BLUE}{pac.epsilon}{ENDC}.
+''')
+
+print(
+    'We can see that desired PAC doesn\'t hold, so the engine can blow up!\n')
 
 print(
     f'''Let\'s look at values violating PAC. Domain PAC verifier can detect values between eps_1
-and eps_2, i. e. values that lie in D±eps_2 \\ D±eps_1. Such values are called highlights.
-Let\'s check highlights for different eps_1, eps_2 values:''')
+and eps_2, i. e. values that lie in D±eps_2 \\ D±eps_1. Such values are called highlights or outliers.
+Let\'s find outliers for different eps_1, eps_2 values:''')
 
 value_ranges = [(0, 1), (1, 2), (2, 3), (3, 5), (5, 7), (7, 10)]
 highlights_table = [(f'{BLUE}{v_range[0]}{ENDC}', f'{BLUE}{v_range[1]}{ENDC}',
@@ -88,36 +137,25 @@ def column_to_str(filename: str) -> str:
 print()
 
 print('''We can see two problems:
-      1. Time engine worked on low temperature was too long, but these temperatures were just a little lower than 80°C.
-      2. Peak temperature was too high, but it has been reached only once.\n'''
-      )
-
-print('''Second version of engine has:
-      1. pre-heating system to prevent engine from working on low temperatures;
-      2. emergency cooling system to lower peak temperatures.
-Let\'s look at second version\'s sensor readings:''')
-print(f'{GRAY}{column_to_str(ENGINE_TEMPS_GOOD)}{ENDC}')
+    1. The engine operated at low temperatures for an extended period, slightly below 80°C.
+    2. The peak temperature was too high, but this occured only once.\n''')
+
+print('''The second version of engine has:
+    1. A pre-heating system to prevent operation at low temperatures.
+    2. An emergency cooling system to limit peak temperatures.
+The updated sensor readings (modified values highlighted) are:''')
+print(f'{display_columns_diff(ENGINE_TEMPS_BAD, 0, ENGINE_TEMPS_GOOD, 0)}')
 print()
 
-print(
-    f'''Let\'s run Domain PAC verifier with same parameters (domain={BLUE}{segment}{ENDC}, max_epsilon={BLUE}10{ENDC}).'''
-)
+print(f'''We run the Domain PAC verifier again.''')
 algo = desbordante.pac_verification.algorithms.DomainPACVerifier()
 algo.load_data(table=(ENGINE_TEMPS_GOOD, ',', True),
                column_indices=[0],
                domain=segment)
-algo.execute(max_epsilon=10, min_delta=0.85)
-
-print(f'Algorithm result: {RED}{algo.get_pac()}{ENDC}.')
-print(
-    f'''This PAC says that epsilon={BLUE}6{ENDC} is enough to cover all possible values. It\'s true, but this information is useless.
-Let\'s select max_epsilon={BLUE}5.5{ENDC} and min_delta={BLUE}0.87{ENDC} to give algorithm a hint which values do we want.'''
-)
-# Max_epsilon is an "execute option", so `load_data` is not needed
-algo.execute(max_epsilon=5.5, min_delta=0.87)
+algo.execute()
 
 print(f'''Algorithm result: {GREEN}{algo.get_pac()}{ENDC}.
-Our desired PAC holds, which means that engine works well.
+The desired PAC now holds, which means the improved engine operates within acceptable limits.
 
-It's recommended to continue with reading second example ({CYAN}examples/basic/verifying_pac/verifying_domain_pac2.py{ENDC}),
+It is recommended to continue with the second example ({CYAN}examples/basic/verifying_pac/verifying_domain_pac2.py{ENDC}),
 which demonstrates more advanced usage of the Parallelepiped domain.''')

examples/basic/verifying_pac/verifying_domain_pac2.py

@@ -9,7 +9,7 @@
 GREEN = '\033[32m'
 BLUE = '\033[34m'
 CYAN = '\033[36m'
-GRAY = '\033[1;30m'
+BOLD = '\033[1;37m'
 ENDC = '\033[0m'
 
 ENGINE_TEMPS = 'examples/datasets/verifying_pac/engine_temps_bad.csv'
@@ -24,71 +24,96 @@ def csv_to_str(filename: str) -> str:
 
 
 print(
-    f'''{CYAN}This example illustrates the usage of Domain Probabilistic Approximate Constraints (PACs).
-This example continues first Domain PAC verification example (examples/basic/verifying_pac/verifying_domain_pac1.py).
-If you haven't read first part, start with reading it.{ENDC}
+    f'''This example illustrates the usage of Domain Probabilistic Approximate Constraints (Domain PACs)
+on multiple columns. It continues the first Domain PAC verification example
+{CYAN}(examples/basic/verifying_pac/verifying_domain_pac1.py){ENDC}. If you have not read the first part yet,
+it is recommended to start there.
 ''')
 
 print(
-    f'''In first example we\'ve verified {BLUE}Domain PAC Pr(x ∈ [85, 95]±5) ≥ 0.9{ENDC} on temperature sensor readings.
-Now we also have tachometer readings:''')
-print(f'{GRAY}{csv_to_str(ENGINE_TEMPS)}{ENDC}')
+    f'''In first example we verified {BLUE}Domain PAC Pr(x ∈ [85, 95]±5) ≥ 0.9{ENDC} on engine temperature sensor readings.
+Now, in addition to temperature readings, we also have tachometer data:''')
+print(f'{BOLD}{csv_to_str(ENGINE_TEMPS)}{ENDC}')
 print()
 
 print(
-    f'''Normal RPM for our engine lie in {BLUE}[1500, 3500]{ENDC}. Values in {BLUE}[0, 5000]{ENDC} are not harmful themselves, but
-cold engine will stall on low RPM and can be damaged on high RPM, and overheated engine can blow up, especially on RPM
-outside of {BLUE}[1500, 3500]{ENDC} (because cooling system operation depends on RPM).
-Let\'s use Domain PAC verifier to check if engine works properly, just like we did in first example.
+    f'''The normal operating RPM for this engine is {BLUE}[1500, 3500]{ENDC}. Values outside this range are
+not harmful by themselves (as long as they are within {BLUE}[0, 5000]{ENDC}), but:
+    * A cold engine may stall at low RPM and can be damaged at high RPM.
+    * An overheated engine is especially vulnerable at RPM values outside [1500, 3500], because
+      cooling efficiency depends on RPM.
+As in the first example, we use the Domain PAC verifier to check whether the engine operates properly.
 ''')
 
 print(
     f'''Firstly we need to create domain. We have a cartesian product of two segments: {BLUE}[85, 95] x [1500, 3500]{ENDC},
 so it would be natural to use parallelepiped.''')
-# Arguments of generic version are A = (a0, a1, ..., an) and B = (b0, b1, ..., bn).
-# Domain is [A, B] = [a0, b0] x [a1, b1] x ... x [an, bn].
+print(
+    f'''We now work with two columns: temperature and RPM. The acceptable operating region is a Cartesian product
+of two segments:
+    * temperature: [85, 95];
+    * RPM: [1500, 3500].
+This forms a parallelepiped domain: {BLUE}[85, 95] x [1500, 3500]{ENDC}.
+''')
+# Arguments of generic version are A = (a1, a2, ..., an) and B = (b1, b2, ..., bn).
+# Domain is [A, B] = [a1, b1] x [a2, b2] x ... x [an, bn].
 parallelepiped = desbordante.pac.domains.Parallelepiped(['85', '1500'],
                                                         ['95', '3500'])
 
 print(
-    f'Let\'s run Domain PAC verifier with domain={BLUE}{parallelepiped}{ENDC}, max_epsilon={BLUE}15{ENDC}, min_delta={BLUE}0.85{ENDC}.'
-)
+    f'''We run the Domain PAC verifier with the following parameters: domain={BLUE}{parallelepiped}{ENDC},
+max_epsilon={BLUE}15{ENDC}.
+''')
 algo = desbordante.pac_verification.algorithms.DomainPACVerifier()
 algo.load_data(table=(ENGINE_TEMPS, ',', True),
                domain=parallelepiped,
                column_indices=[0, 1])
-algo.execute(max_epsilon=15, min_delta=0.85)
+algo.execute(max_epsilon=10)
 pac = algo.get_pac()
 print(f'Algorithm result: {RED}{pac}{ENDC}.')
 print(
-    'Delta is less than min_delta? What does it mean? Let\'s look at highlights:'
+    f'A result with δ = {BLUE}{pac.delta}{ENDC} is unexpected. To understand what is happening, we examine the highlights.'
 )
 
-# Default values are eps_1 = min_epsilon and eps_2 = pac.epsilon
 print(
-    f'Highlights between {BLUE}0{ENDC} and {BLUE}{pac.epsilon}{ENDC}: {algo.get_highlights()}\n'
-)
-print(f'''There are no highlights! Maybe we\'ve selected wrong parameters?
-Which epsilon should we use: {BLUE}10{ENDC} for temperatures or {BLUE}1500{ENDC} for RPM? We\'ll need some math to answer this.
-
-Parallelepiped uses Chebyshev metric to calculate distance between value tuples: {GRAY}d(x, y) = max{{|x[0] - y[0]|, ..., |x[n] - y[n]|}}{ENDC}.
-But in our case difference between RPM values will always be greater than difference between temperatures!
-For such situations all coodinate-wise-metric-based domains (currently it's Parallelepiped and Ball, but you can
-define your own in C++) have additional parameter: list of levelling coefficients. When it\'s passed,
-distance becomes {GRAY}d(x, y) = max{{|x[0] - y[0]| * lc[0], ..., |x[n] - y[n]| * lc[n]}}{ENDC}.
-
-Let\'s use levelling_coefficients={BLUE}[1, 0.01]{ENDC} to normalize temperatures and RPM.'''
-      )
-# Also parallelepiped uses product compare: x < y iff x[0] < y[0] & ... & x[n] < y[n]
+    f'''Highlights between {BLUE}0{ENDC} and {BLUE}{pac.epsilon}{ENDC} are: {BOLD}{algo.get_highlights(0, pac.epsilon)}{ENDC}.
+''')
+print(
+    f'''There are very few hihglights, which suggests that the parameters may not be chosen correctly.
+
+The question is: what does ε = {BLUE}{pac.epsilon}{ENDC} mean in two-dimensional domain? Should ε correspond to:
+    * 10 degrees of temperature difference, or
+    * 1500 RPM difference?
+To answer this, we need to understand how distnace is computed.
+
+The parallelepiped uses the Chebyshev metric to calculate distance between value tuples:
+    {BOLD}d(x, y) = max{{|x[1] - y[1]|, ..., |x[n] - y[n]|}}{ENDC}
+In our case:
+    * temperature differences are on the order of tens;
+    * RPM differences are on the order of thousands.
+As a result, RPM differences dominate the distance computation, making temperature differences
+almost irrelevant. This issue affects all coordinate-wise metric-based domains (currently
+Parallelepiped and Ball, though custom domains can be implemented in C++).
+
+To address this, such domains support {CYAN}levelling coefficients{ENDC}, which rescale individual
+dimensions. With levelling coefficients, the distance becomes:
+    {BOLD}d(x, y) = max{{|x[1] - y[1]| * lc[1], ..., |x[n] - y[n]| * lc[n]}}{ENDC}
+To normalize temperatures and RPM scales, we use levelling_coefficients={BLUE}[1, 0.01]{ENDC} parameter.
+This treats a 100 RPM difference as comparable to a 1°C difference.
+
+With levelling coefficients applied, we rerun the algorithm.
+''')
+
 parallelepiped = desbordante.pac.domains.Parallelepiped(['85', '1500'],
                                                         ['95', '3500'],
                                                         [1, 0.01])
 algo = desbordante.pac_verification.algorithms.DomainPACVerifier()
 algo.load_data(table=(ENGINE_TEMPS, ',', True),
                domain=parallelepiped,
                column_indices=[0, 1])
-algo.execute(max_epsilon=15, min_delta=0.85)
+algo.execute(max_epsilon=10, min_delta=0.9)
 print(f'''Algorithm result: {GREEN}{algo.get_pac()}{ENDC}.
+This result is now meaningful and consistent with the findings from the first example.
 
-Now it\'s recommended to continue with reading third example ({CYAN}examples/basic/verifying_pac/verifying_domain_pac3.py{ENDC}),
-which introduces another basic domain: Ball.''')
+It is recommended to continue with the third example ({CYAN}examples/basic/verifying_pac/verifying_domain_pac3.py{ENDC}),
+which introduces another basic domain type: Ball.''')

examples/datasets/verifying_pac/engine_temps_good.csv

@@ -11,7 +11,7 @@ t
 89
 94
 96
-101
+100
 93
 90
 88