#!/usr/bin/env python
#
# Copyright (c) 2015-2019 Artur Meski
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in all
# copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.
#

from rs import *
from smt import *
from logics import *
from rsltl_shortcuts import *

from itertools import chain, combinations

import sys
import resource


def generate_system(chainLen, maxConc):
    """
    This function generates the reaction system with concentrations
    for the scalable chain benchmark

    chainLen is the length of the chain
    maxConc is the maximal concentration
    """

    r = ReactionSystemWithConcentrations()
    r.add_bg_set_entity(("inc", 1))
    r.add_bg_set_entity(("dec", 1))

    for i in range(1, chainLen + 1):
        r.add_bg_set_entity(("e_" + str(i), maxConc))

    for i in range(1, chainLen + 1):
        ent = "e_" + str(i)
        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)])
        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
        if i < chainLen:
            r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])

    r.add_reaction(
        [("e_" + str(chainLen), maxConc)],
        [("dec", 1)],
        [("e_" + str(chainLen), maxConc)],
    )

    c = ContextAutomatonWithConcentrations(r)
    c.add_init_state("init")
    c.add_state("working")
    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
    c.add_transition("working", [("inc", 1)], "working")

    rc = ReactionSystemWithAutomaton(r, c)

    return rc


def generate_formula(formula_number, chainLen, maxConc):
    """
    This function generates the rsLTL formula
    corresponding to the formula_number parameter
    """

    if formula_number == 1:
        ret = Formula_rsLTL.f_F(
            BagDescription.f_entity("inc") > 0,
            (BagDescription.f_entity("e_" + str(chainLen)) >= maxConc),
        )

    elif formula_number == 2:
        f_tmp = Formula_rsLTL.f_F(
            BagDescription.f_entity("inc") > 0,
            (BagDescription.f_entity("e_" + str(chainLen)) == maxConc),
        )
        for i in range(chainLen - 1, 0, -1):
            f_tmp = Formula_rsLTL.f_F(
                BagDescription.f_entity("inc") > 0,
                f_tmp & (BagDescription.f_entity("e_" + str(i)) == maxConc),
            )
        ret = f_tmp

    elif formula_number == 3:
        ret = Formula_rsLTL.f_G(
            BagDescription.f_TRUE(),
            Formula_rsLTL.f_Implies(
                (BagDescription.f_entity("e_1") == 1),
                Formula_rsLTL.f_F(
                    BagDescription.f_entity("inc") > 0,
                    (BagDescription.f_entity("e_" + str(chainLen)) == maxConc),
                ),
            ),
        )

    elif formula_number == 4:
        ret = Formula_rsLTL.f_F(
            BagDescription.f_entity("inc") > 0,
            BagDescription.f_entity("e_1") == maxConc,
        )

    elif formula_number == 5:
        ret = Formula_rsLTL.f_X(
            BagDescription.f_TRUE(),
            Formula_rsLTL.f_U(
                BagDescription.f_entity("inc") > 0,
                BagDescription.f_entity("e_1") > 0,
                BagDescription.f_entity("e_2") > 0,
            ),
        )

    else:
        ret = None

    assert ret is not None, "Unknown formula"

    return ret


def save_statistics(smt_rsc, formula_number, chainLen, maxConc):
    """
    Saves the statistics fetched from smt_rsc into files
    """
    time = 0
    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
    filename_t = "bench_rsc_F" + str(formula_number) + "_time.log"
    filename_m = "bench_rsc_F" + str(formula_number) + "_mem.log"
    time = smt_rsc.get_verification_time()

    f = open(filename_t, "a")
    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
    f.write(log_str)
    f.close()

    f = open(filename_m, "a")
    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
    f.write(log_str)
    f.close()


def scalable_chain(print_system=False):
    """
    This is the entry point for the benchmark
    """
    if len(sys.argv) < 1 + 3:
        print("arguments: <chainLen> <maxConc> <formulaNumber>")
        exit(1)

    chainLen = int(sys.argv[1])  # chain length
    maxConc = int(sys.argv[2])  # depth (max concentration)
    formula_number = int(sys.argv[3])

    if chainLen < 1 or maxConc < 1:
        print("be reasonable")
        exit(1)
    if not formula_number in range(1, 5 + 1):
        print("formulaNumber must be in 1..5")
        exit(1)

    # Generate the reaction systems with concentrations
    rc = generate_system(chainLen, maxConc)

    # Generate the formula
    form = generate_formula(formula_number, chainLen, maxConc)

    # Optional dump/print of the system
    if print_system:
        rc.show()

    # Create an instance of the SMT checker for RS with concentrations
    smt_rsc = SmtCheckerRSC(rc)

    # Start the verification process
    smt_rsc.check_rsltl(formula=form)

    save_statistics(smt_rsc, formula_number, chainLen, maxConc)


def main():
    scalable_chain(print_system=True)


if __name__ == "__main__":
    main()