<commit_before>"""
Copyright (C) 2017 <NAME> <<EMAIL>>

This file is distributed under the terms of the 3-clause BSD License.
A copy of the license can be found in the root directory or at
https://opensource.org/licenses/BSD-3-Clause.

Author: <NAME> <<EMAIL>>
  Date: 27/03/2017

Entry point
"""

import argparse as ap
import os
import importlib
import pandas as pd
import colorama as cl
import config
import intrepyd.colors as ic
import intrepyd.lustre2py.translator as tr
import intrepyd.api as api
import intrepyd.engine as en
import intrepyd
import multiprocessing as mp
import time
import random as rm


global_ctx = intrepyd.Context()


def parse_arguments():
    """
    Command-line parser
    """
    arg_parser = ap.ArgumentParser(prog='intrepyd',
                                   formatter_class=ap.ArgumentDefaultsHelpFormatter)
    arg_parser.add_argument('INFILE',
                            help='The input file to process')
    arg_parser.add_argument('-c', '--config', default='config.json',
                            help='Specifies a config file')
    return arg_parser.parse_args()


def translate_simulink(ctx, infile):
    """
    Translates a simulink file into intrepyd syntax
    """
    raise NotImplementedError
    return None


def translate_lustre(ctx, infile, topnode):
    """
    Translates a lustre file into intrepyd syntax
    """
    outmodule = 'encoding'
    outfilename = outmodule + '.py'
    tr.translate(infile, topnode, outfilename)
    enc = importlib.import_module(outmodule)
    return enc.lustre2py_main(ctx)


def translate_infile(ctx, infile, cfg):
    """
    Translates an input file depending on the suffix
    """
    outputs = None
    if infile[-4:] == '.slx' or infile[-4:] == '.mdl':
        outputs = translate_simulink(ctx, infile)
    elif infile[-4:] == '.lus' or infile[-4:] == '.ec':
        outputs = translate_lustre(ctx, infile, cfg['lustre.topnode'])
    else:
        raise RuntimeError('Did not recognize a file extension in [slx, mdl, lus, ec]')
    return outputs


def simulate(ctx, infile, cfg, verbose, outputs):
    """
    Simulates the design using default values for inputs or by taking
    input values from an existing simulation file
    """
    sim_file = os.path.basename(infile) + '.csv'
    trace = ctx.mk_trace()
    depth = cfg["simulation.depth"]
    if os.path.isfile(sim_file):
        if verbose:
            print 'Re-simulating using input values from ' + sim_file
        sim_data = pd.read_csv(sim_file, index_col=0)
        depth = trace.set_from_dataframe(sim_data, ctx.inputs)
    else:
        if verbose:
            print 'Simulating using default values into ' + sim_file
        dpt = 0
        while dpt <= depth:
            for _, net in ctx.inputs.iteritems():
                trace.set_value(net, dpt, 'false')
            dpt += 1
    simulator = ctx.mk_simulator()
    for output in outputs:
        simulator.add_watch(output)
    simulator.simulate(trace, depth)
    dataframe = trace.get_as_dataframe(ctx.net2name)
    dataframe.to_csv(sim_file)
    if verbose:
        print 'Simulation result written to ' + sim_file
    print dataframe

def main():
    """
    Main
    """
    parsed_args = parse_arguments()
    cfg = config.Config.get_instance(parsed_args.config)
    verbose = cfg["verbose"]
    if verbose:
        print 'Parsing input file'
    ctx = intrepyd.Context()
    outputs = translate_infile(ctx, parsed_args.INFILE, cfg)
    bad = ctx.mk_not(outputs)
    breach = ctx.mk_backward_reach()
    breach.add_target(bad)
    result = breach.reach_targets()
    print result

if __name__ == "__main__":
    cl.init()
    try:
        main()
    except:
        print ic.fail('ABORTED')
        raise<commit_msg>Cleaned main<commit_after>"""
Copyright (C) 2017 <NAME> <<EMAIL>>

This file is distributed under the terms of the 3-clause BSD License.
A copy of the license can be found in the root directory or at
https://opensource.org/licenses/BSD-3-Clause.

Author: <NAME> <<EMAIL>>
  Date: 27/03/2017

Entry point
"""

import argparse as ap
import os
import importlib
import pandas as pd
import colorama as cl
import config
import intrepyd.colors as ic
import intrepyd.lustre2py.translator as tr
import intrepyd.api as api
import intrepyd.engine as en
import intrepyd
import multiprocessing as mp
import time
import random as rm


global_ctx = intrepyd.Context()


def parse_arguments():
    """
    Command-line parser
    """
    arg_parser = ap.ArgumentParser(prog='intrepyd',
                                   formatter_class=ap.ArgumentDefaultsHelpFormatter)
    arg_parser.add_argument('INFILE',
                            help='The input file to process')
    arg_parser.add_argument('-c', '--config', default='config.json',
                            help='Specifies a config file')
    return arg_parser.parse_args()


def translate_simulink(ctx, infile):
    """
    Translates a simulink file into intrepyd syntax
    """
    raise NotImplementedError
    return None


def translate_lustre(ctx, infile, topnode):
    """
    Translates a lustre file into intrepyd syntax
    """
    outmodule = 'encoding'
    outfilename = outmodule + '.py'
    tr.translate(infile, topnode, outfilename)
    enc = importlib.import_module(outmodule)
    return enc.lustre2py_main(ctx)


def translate_infile(ctx, infile, cfg):
    """
    Translates an input file depending on the suffix
    """
    outputs = None
    if infile[-4:] == '.slx' or infile[-4:] == '.mdl':
        outputs = translate_simulink(ctx, infile)
    elif infile[-4:] == '.lus' or infile[-4:] == '.ec':
        outputs = translate_lustre(ctx, infile, cfg['lustre.topnode'])
    else:
        raise RuntimeError('Did not recognize a file extension in [slx, mdl, lus, ec]')
    return outputs


def simulate(ctx, infile, cfg, verbose, outputs):
    """
    Simulates the design using default values for inputs or by taking
    input values from an existing simulation file
    """
    sim_file = os.path.basename(infile) + '.csv'
    trace = ctx.mk_trace()
    depth = cfg["simulation.depth"]
    if os.path.isfile(sim_file):
        if verbose:
            print 'Re-simulating using input values from ' + sim_file
        sim_data = pd.read_csv(sim_file, index_col=0)
        depth = trace.set_from_dataframe(sim_data, ctx.inputs)
    else:
        if verbose:
            print 'Simulating using default values into ' + sim_file
        dpt = 0
        while dpt <= depth:
            for _, net in ctx.inputs.iteritems():
                trace.set_value(net, dpt, 'false')
            dpt += 1
    simulator = ctx.mk_simulator()
    for output in outputs:
        simulator.add_watch(output)
    simulator.simulate(trace, depth)
    dataframe = trace.get_as_dataframe(ctx.net2name)
    dataframe.to_csv(sim_file)
    if verbose:
        print 'Simulation result written to ' + sim_file
    print dataframe

def main():
    """
    Main
    """
    parsed_args = parse_arguments()
    cfg = config.Config.get_instance(parsed_args.config)
    verbose = cfg["verbose"]
    if verbose:
        print 'Parsing input file'
    ctx = intrepyd.Context()
    outputs = translate_infile(ctx, parsed_args.INFILE, cfg)
    bad = ctx.mk_not(outputs)
    breach = ctx.mk_backward_reach()
    breach.add_target(bad)
    result = breach.reach_targets()
    if result == en.EngineResult.UNREACHABLE:
         print 'Safe'
    elif result == en.EngineResult.REACHABLE:
         print 'Unsafe'
    else:
         print 'Unknown'

if __name__ == "__main__":
    cl.init()
    try:
        main()
    except:
        print ic.fail('ABORTED')
        raise
{'fraction_non_alphanumeric': 0.10273524407800026, 'fraction_numerical': 0.006281900274833137, 'mean_word_length': 2.7497546614327772, 'pattern_counts': {'":': 2, '<': 17, '<?xml version=': 0, '>': 15, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5717417', 'n_tokens_mistral': 2447, 'n_tokens_neox': 2356, 'n_words': 669}