"""
# Author: CoLoMoTo
# Affiliation: CoLoMoTo
# Aim: Export a GINsim model into NuSMV-compatible format, and check a set of properties.
# Date: 26/03/2018
# Run: snakemake --reason --snakefile ./SnakeMake/Snakefile_GINsim-SS_NuSMV
"""


import os, os.path, time, subprocess

#########################
# Variables

# Folders
BASEDIR = os.getcwd()
TAG = time.strftime("%Y%m%d%H%M%S")
OUTDIR = "%s_output" % (TAG)

# Docker
# Name of the Docker image
COLOMOTOIMG = "colomoto/colomoto-docker:next"
# Name of the created Docker container
COLOMOTOCONT = "colomoto-container-%s" % (TAG)

# Tools
GINSIM = "GINsim" # available in docker image
GINSIM_EXPORT_AS_NUSMV = "Scripts/ginsim_export_as_NuSMV.py"
NUSMV = "NuSMV" # available in docker image
NUSMV_REPORT = "Scripts/nusmv_report_all_tests.py"

# I/O Files
MODELDIR = "Models/2016_CellCycle_Traynard/"
ginsimModel = "Traynard_MultiLevel_MamCC_Apr2016"


#########################
# Rules 


# This rule will be executed last. But to run it, it needs to create the input files beforehand.
rule all:
	message: "\n##########\n# Final rule."
	input:
		"{outputDir}/{modelName}_stableStates.txt".format(outputDir=OUTDIR, modelName=ginsimModel),
		"{outputDir}/{modelName}_NuSMV_report.txt".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"docker stop {COLOMOTOCONT}"

# Pull CoLoMoTo Docker image from DockerHub
# Output : A flag file indicating that the image is available
rule pull_colomoto_image:
	message:
		"\n##########\n# Pull CoLoMoTo image from DockerHub"
	output:
		"{outputDir}/CoLoMoTo_image_available".format(outputDir=OUTDIR)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker pull {COLOMOTOIMG} && docker run --rm -d --name={COLOMOTOCONT} -v {BASEDIR}:/home -ti {COLOMOTOIMG} /bin/bash && "
		"touch {output}"


# Find stable states of a GINsim model
# Input : GINsim model
# Output : Export NuSMV
rule ginsim_find_SS:
	message:
		"\n##########\n# Find Stable States of {input.model} using GINsim"
	input:
		docker_image = "{outputDir}/CoLoMoTo_image_available".format(outputDir=OUTDIR),
		model = "{modelDir}/{modelName}.zginml".format(modelDir=MODELDIR, modelName=ginsimModel)
	output:
		"{outputDir}/{modelName}_stableStates.txt".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker exec {COLOMOTOCONT} {GINSIM} -lm /home/{input.model} -r stable 1>>{output}"


# Export a GINsim model as NuSMV format
# Input : GINsim model
# Output : Export NuSMV
rule ginsim_export_as_nusmv:
	message:
		"\n##########\n# Export {input.model} in NuSMV format as {output}"
	input:
		docker_image = "{outputDir}/CoLoMoTo_image_available".format(outputDir=OUTDIR),
		model = "{modelDir}/{modelName}.zginml".format(modelDir=MODELDIR, modelName=ginsimModel)
	output:
		"{outputDir}/{modelName}_NuSMV_export.smv".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker exec {COLOMOTOCONT} python3 /home/{GINSIM_EXPORT_AS_NUSMV} /home/{input.model} /home/{output}"

# Concatenate exported model with properties to be tested
# Input : Model in SMV format; NuSMV properties
# Output : Concatenated files
rule concatenate_NuSMV_model_properties:
	message:
		"\n##########\n# Concatenate exported GINsim model {input.model} with properties to be tested {input.property} into {output}"
	input:
		docker_image = "{outputDir}/CoLoMoTo_image_available".format(outputDir=OUTDIR),
		model = "{outputDir}/{modelName}_NuSMV_export.smv".format(outputDir=OUTDIR, modelName=ginsimModel),
		property = "{modelDir}/{modelName}_property.smv".format(modelDir=MODELDIR, modelName=ginsimModel)
	output:
		"{outputDir}/{modelName}_NuSMV_property.smv".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker exec {COLOMOTOCONT} cat /home/{input.model} /home/{input.property} > {output}"


# Test NuSMV properties
# Input : model+properties to test; flag file indicating that the docker image is present
# Output : NuSMV output redirected from 
rule test_property:
	message:
		"\n##########\n# Run NuSMV"
	input:
		docker_image = "{outputDir}/CoLoMoTo_image_available".format(outputDir=OUTDIR),
		model = "{outputDir}/{modelName}_NuSMV_property.smv".format(outputDir=OUTDIR, modelName=ginsimModel)
	output:
		"{outputDir}/{modelName}_NuSMV_output.txt".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker exec {COLOMOTOCONT} {NUSMV} /home/{input.model} > {output}"

# Create report
rule report_nusmv:
	message:
		"\n##########\n# Report NuSMV results"
	input:
		"{outputDir}/{modelName}_NuSMV_output.txt".format(outputDir=OUTDIR, modelName=ginsimModel)
	output:
		"{outputDir}/{modelName}_NuSMV_report.txt".format(outputDir=OUTDIR, modelName=ginsimModel)
	shell:
		"mkdir -p {OUTDIR} && "
		"docker exec {COLOMOTOCONT} python3 /home/{NUSMV_REPORT} -o /home/{output} /home/{input}"
