From f6c1024b30473dfe81141f5ebf7d042e753c3afc Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 2 Feb 2022 12:47:25 +0100 Subject: [PATCH] Some more cleanup --- satuio/ads.py | 45 ++++++++++---------------------- satuio/uio-incr.py | 27 +++++-------------- satuio/uio.py | 37 ++++++++------------------ satuio/{ => utils}/parser.py | 0 satuio/utils/utils.py | 50 ++++++++++++++++++++++++++++++++++++ 5 files changed, 81 insertions(+), 78 deletions(-) rename satuio/{ => utils}/parser.py (100%) create mode 100644 satuio/utils/utils.py diff --git a/satuio/ads.py b/satuio/ads.py index 7d7f8e8..41648bc 100644 --- a/satuio/ads.py +++ b/satuio/ads.py @@ -22,19 +22,10 @@ from pysat.card import CardEnc, EncType from argparse import ArgumentParser # Command line options from rich.console import Console # Import colorized output -from time import time # Time for rough timing measurements from tqdm import tqdm # Import fancy progress bars -from parser import read_machine - -# function for some time logging -start = time() -start_total = start -def measure_time(*str): - global start - now = time() - print('***', *str, "in %.3f seconds" % (now - start)) - start = now +from utils.parser import read_machine +from utils.utils import * # ***************** @@ -45,8 +36,8 @@ def measure_time(*str): parser = ArgumentParser() parser.add_argument('filename', help='File of the mealy machine (dot format)') parser.add_argument('length', help='Length of the ADS', type=int) -parser.add_argument('-v', '--verbose', help="Show more output", action='store_true') -parser.add_argument('--show-differences', help="Show even more output", action='store_true') +parser.add_argument('-v', '--verbose', help='Show more output', action='store_true') +parser.add_argument('--show-differences', help='Show even more output', action='store_true') parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3') parser.add_argument('--states', help='For which states to compute an ADS', nargs='+') args = parser.parse_args() @@ -259,15 +250,11 @@ measure_time('Solver finished') # are no assumptions used in our encoding. if not solution: console.print('! no ADS of length', length, style='bold red') + measure_total_time('Done') exit() -# We get the model, and store all true variables -# in a set, for easy lookup. -m = solver.get_model() -truth = set() -for l in m: - if l > 0: - truth.add(l) +# Get the set of true variables +truth = get_truth(solver) # (If verbose) For each state, we print the paths and output. # We mark the differences red (there can be differences not @@ -325,12 +312,6 @@ if args.show_differences: console.print('') -# Get some element from a set, doesn't matter which -def some_elem(collection): - for x in collection: - return x - - # Now we will extract the tree from the solution above. # The initial_set indicates which states we possibly started at, # and the level is the current depth of the tree. @@ -365,7 +346,8 @@ def extract_tree(initial_set, level): return { 'split_symbol': split_symbol, 'subtree': sub_trees } -# Pretty (and compactly) printing the tree +# Pretty (and compactly) printing the tree. As before, we color code +# the output: green for inputs, red for outputs, and blue for states def print_tree(console, tree, left=''): # The leaf is inlined in the printing if 'leaf' in tree: @@ -394,14 +376,13 @@ def print_tree(console, tree, left=''): print_tree(console, subtree, left + str_pad) -# Output the full tree +# Output the distinguishing tree print_tree(console, extract_tree(states, 0)) - +print('') # Report some final stats -start = start_total -print('') -measure_time("Done with total time") +measure_total_time('Done') + # TODO: we know that dvar(s, t, i) is an equivalence relation for # each i. Do we help the solver when asserting that? Or will that diff --git a/satuio/uio-incr.py b/satuio/uio-incr.py index 46248db..5c9e6ba 100644 --- a/satuio/uio-incr.py +++ b/satuio/uio-incr.py @@ -22,23 +22,15 @@ from pysat.card import CardEnc, EncType from argparse import ArgumentParser # Command line options from rich.console import Console # Import colorized output -from time import time # Time for rough timing measurements from tqdm import tqdm # Import fancy progress bars -from parser import read_machine +from utils.parser import read_machine +from utils.utils import * + # We set up some things for nice output console = Console(markup=False, highlight=False) -# function for some time logging -start = time() -start_total = start -def measure_time(*str): - global start - now = time() - print('***', *str, "in %.3f seconds" % (now - start)) - start = now - # ***************** # Reading the input @@ -355,13 +347,8 @@ for length in range(2, bound + 1): if not b: continue - # We get the model, and store all true variables - # in a set, for easy lookup. - m = solver.get_model() - truth = set() - for l in m: - if l > 0: - truth.add(l) + # Get the set of true variables + truth = get_truth(solver) # We extract the word uio = [] @@ -381,9 +368,9 @@ for length in range(2, bound + 1): for (s, uio) in uios.items(): console.print(s, style='bold black', end=' => ') console.print(uio, style='bold green') +print('') # Report some final stats -start = start_total -measure_time("Done with total time") +measure_total_time('\nDone') print('With UIO:', len(uios)) print('without: ', len(states) - len(uios)) diff --git a/satuio/uio.py b/satuio/uio.py index f1a25c4..84477af 100644 --- a/satuio/uio.py +++ b/satuio/uio.py @@ -4,7 +4,7 @@ Script for finding UIO sequences in a Mealy machine. Uses SAT solvers but you can specify multiple (or all) states for which an UIO is desired. When an UIO (of specified length) does not exist, the solver returns UNSAT. For the usage, please run - + python3 uio.py --help © Joshua Moerman, Open Universiteit, 2022 @@ -17,19 +17,10 @@ from pysat.card import CardEnc, EncType from argparse import ArgumentParser # Command line options from rich.console import Console # Import colorized output -from time import time # Time for rough timing measurements from tqdm import tqdm # Import fancy progress bars -from parser import read_machine - -# function for some time logging -start = time() -start_total = start -def measure_time(*str): - global start - now = time() - print('***', *str, "in %.3f seconds" % (now - start)) - start = now +from utils.parser import read_machine +from utils.utils import * # ***************** @@ -40,7 +31,7 @@ def measure_time(*str): parser = ArgumentParser() parser.add_argument('filename', help='File of the mealy machine (dot format)') parser.add_argument('length', help='Length of the UIO', type=int) -parser.add_argument('-v', '--verbose', help="Show more output", action='store_true') +parser.add_argument('-v', '--verbose', help='Show more output', action='store_true') parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3') parser.add_argument('--bases', help='For which states to compute an UIO (leave empty for all states)', nargs='*') args = parser.parse_args() @@ -171,7 +162,7 @@ for s in tqdm(states, desc="CNF paths"): # x_('s', s, i, t) /\ x_('in', i, a) => x_('s', s, i+1, delta(t, a)) # == -x_('s', s, i, t) \/ -x_('in', i, a) \/ x_('s', s, i+1, delta(t, a)) solver.add_clause([-sv, -av, svar(s, i+1, next_t)]) - + # Only one output should be enabled unique([ovar(s, i, o) for o in possible_outputs[(s, i)]]) @@ -243,14 +234,9 @@ for base in bases: measure_time('Solver finished') if b: - # We get the model, and store all true variables - # in a set, for easy lookup. - m = solver.get_model() - truth = set() - for l in m: - if l > 0: - truth.add(l) - + # Get the set of true variables + truth = get_truth(solver) + # We print the word console.print('! UIO of length', length, style='bold green') for i in range(length): @@ -278,7 +264,7 @@ for base in bases: style = 'bold green' elif evar(s, i) in truth: style = 'bold red' - + console.print(o, end=', ', style=style) console.print('') @@ -287,10 +273,9 @@ for base in bases: # The core returned by the solver is not interesting: # It is only the assumption (i.e. bvar). +print('') # Report some final stats -start = start_total -print('') -measure_time("Done with total time") +measure_total_time('\nDone') print('With UIO:', num_uios[True]) print('without: ', num_uios[False]) diff --git a/satuio/parser.py b/satuio/utils/parser.py similarity index 100% rename from satuio/parser.py rename to satuio/utils/parser.py diff --git a/satuio/utils/utils.py b/satuio/utils/utils.py new file mode 100644 index 0000000..e17ad12 --- /dev/null +++ b/satuio/utils/utils.py @@ -0,0 +1,50 @@ +""" +Functions to measure time and print stuff nicely, etc + +© Joshua Moerman, Open Universiteit, 2022 +""" + +from time import time + +# ******************************* +# Functions for some time logging +# ******************************* + +start = time() +start_total = start + +def measure_time(*str): + global start + now = time() + print('***', *str, "in %.3f seconds" % (now - start)) + start = now + +def measure_total_time(*str): + global start_total + now = time() + print('***', *str, ": total time = %.3f seconds" % (now - start_total)) + + +# **************************** +# Functions related to solving +# **************************** + +# This stores all true variables in a set, for easy lookup +def get_truth(solver): + m = solver.get_model() + truth = set() + for l in m: + if l > 0: + truth.add(l) + return truth + + +# ***************** +# General functions +# ***************** + +# Get some element from a set, doesn't matter which. +# (I could not find this in the standard library.) +def some_elem(collection): + for x in collection: + return x