@sew< workflow , 1.0 >:

// Symbolic Execution Workflow
// Diversity Tool Configuration
// CEA - LIST
workflow {
	workspace [
		root   = "C:/Diversity/TP/workspace-training/Diversity"
		output = "SymbolicExecution/Output"
		log    = "log"
		debug  = "debug"
	] // end workspace
	director behavior#selection 'as main execution objective' {
		manifest [
			autoconf  = true
			autostart = true
		] // end manifest
		project 'path of input model' [
			source = "C:/Diversity/TP/workspace-training/Diversity/Specification"
			model  = "thermostatSystem.xlia"
		] // end project
		supervisor {
			limit 'of graph exploration' [
				step = 1000
				eval = 1000
				height = 7
			] // end limit
			queue 'defining the exploration/search strategy' [
				strategy = 'WEIGHT#BREADTH_FIRST_SEARCH'
				heuristic = true
			] // end queue
			redundancy 'detection strategy' [
				loop#detection#trivial = true
			] // end redundancy
			console [
				format = "\nstep:%1% , context:%2% , height:%3% , width:%4%"
				report = "\nstop:%1% , context:%2% , height:%3% , width:%4%"
			] // end console
		}
		worker [
			coverage#behavior behavior_coverage {
				property [
					stop  = true
					slice = true
					heuristic = true
					scope = 'GLOBALLY'
					scheduler = '|;|'
				] // end property
				trace [
					// Sequence of elements (separated by newline or semicolon)
					// characterizing the desired behavior.
					// The elements of the sequence may be selected from:
					transition = "e22"
					state = "<state-name-id>"
					input = "<input-port-or-signal-name-id>"
					inout = "<inout-port-or-signal-name-id>"
					output = "<output-port-or-signal-name-id>"
					com = "<input-or-output-port-or-signal-name-id>"
				] // end trace
				heuristic [
					hit#consecutive = false
					hit#folding = true
					hit#lucky   = false
					hit#max     = false
					jump#slice  = false
					jump#height = 5
					jump#trials#limit = -1
					hit#count  = 1
					jump#count = 1
				] // end heuristic
				console [
					format = " , coverage: %1% / %2%"
				] // end console
			}
			serializer#symbex#graphviz symbex2graphiz {
				property [
					info#selection = 'ALL'
					data#selection = 'MODIFIED'
				] // end property
				trace [
					com = "[*]"
					variable = "[*]"
					path#condition = "PC: %1%"
					path#timed#condition = "PtC: %1%"
					// See full grammar of [Trace Specification] at the end of this generated file
				] // end trace
				format [
					node#header = "EC#%1%<Ev:%2% , H:%3%>\n%6%"
					lifeline#state = "%2%:%4%"
					path#condition = "PC: %1%"
					path#timed#condition = "PtC: %1%"
					node#condition = "NC: %1%"
					node#timed#condition = "NtC: %1%"
					assign = "%3%=%4%"
					newfresh = "newfresh(%2%:%3%) <- %4%"
					input#env = "INPUT %2%:%3%%4%"
					input#rdv = "input %2%:%3%%4%"
					input = "input %2%:%3%%4%"
					output#env = "OUTPUT %2%:%3%%4%"
					output#rdv = "output %2%:%3%%4%"
					output = "output %2%:%3%%4%"
					routine = "invoke %2%:%3%"
					transition = "fired transition %3%"
					machine = "run %2%:%3%"
				] // end format
				css [
					node#color = 'lightblue'
					node#shape = 'ellipse'
					node#style = 'filled'
					node#passed#color = 'yellow'
					node#passed#shape = 'ellipse'
					node#passed#style = 'filled'
					node#failed#color = 'red'
					node#failed#shape = 'doubleoctagon'
					node#failed#style = 'filled'
					node#inconclusive#color = 'orange'
					node#inconclusive#shape = 'octagon'
					node#inconclusive#style = 'filled'
					node#aborted#color = 'red'
					node#aborted#shape = 'octagon'
					node#aborted#style = 'filled'
					node#warning#color = 'orange'
					node#warning#shape = 'ellipse'
					node#warning#style = 'filled'
					node#error#color = 'red'
					node#error#shape = 'ellipse'
					node#error#style = 'filled'
					node#alert#color = 'red'
					node#alert#shape = 'ellipse'
					node#alert#style = 'filled'
					node#exit#color = 'orange'
					node#exit#shape = 'tripleoctagon'
					node#exit#style = 'filled'
					node#redundancy#source#color = 'green'
					node#redundancy#source#shape = 'cds'
					node#redundancy#source#style = 'filled'
					node#redundancy#target#color = 'greenyellow'
					node#redundancy#target#shape = 'septagon'
					node#redundancy#target#style = 'filled'
					path#passed#color = 'lawngreen'
					path#passed#shape = 'tripleoctagon'
					path#passed#style = 'filled'
					path#failed#color = 'red'
					path#failed#shape = 'doubleoctagon'
					path#failed#style = 'filled'
					path#inconclusive#color = 'orange'
					path#inconclusive#shape = 'octagon'
					path#inconclusive#style = 'filled'
					path#aborted#color = 'red'
					path#aborted#shape = 'octagon'
					path#aborted#style = 'filled'
				] // end css
				vfs [
					file = "symbex_output.gv"
				] // end vfs
			}
			serializer#symbex#trace#basic basic_trace_generator {
				property [
					solver = 'CVC4'
					format = 'BASIC'
					info#selection = 'ALL'
					data#selection = 'MODIFIED'
					numerizer = 'SOLVER'
					normalize = true
					print#initial#values = false
					print#lifelines = false
				] // end property
				format [
					comment = "\t// %1%\n"
					path#condition = "\tPC: %1%\n"
					path#timed#condition = "\tPtC: %1%\n"
					node#condition = "\tNC: %1%\n"
					node#timed#condition = "\tNtC: %1%\n"
					time = "\tdelta = %4%\n"
					assign = "\t%3%=%4%\n"
					newfresh = "\tnewfresh(%2%:%3%) <- %4%\n"
					input#env = "\tINPUT  %3%%4%\n"
					input#rdv = "\tinput  %2%:%3%%4%\n"
					input = "\tinput  %2%:%3%%4%\n"
					output#env = "\tOUTPUT %3%%4%\n"
					output#rdv = "\toutput %3%%4%\n"
					output = "\toutput %3%%4%\n"
					routine = "\tinvoke %2%:%3%\n"
					transition = "\tfired transition %2%:%3%\n"
					machine = "\trun %2%:%3%\n"
				] // end format
				trace [
					// See full grammar of [Trace Specification] at the end of this generated file
					time = "[*]"
					input#env = "[*]"
					// See full grammar of [Trace Specification] at the end of this generated file
				] // end trace
				vfs [
					folder = "ScenarioFiles"
					file   = "scenario_all.txt"
				] // end vfs
			}
		] // end worker
	}
	symbex 'option' [
		name_id_separator = "_"   // default "#"
		newfresh_param_name_pid = false
		pretty_printer_var_name = true   // default false
		time_name_id = '$time'
		delta_name_id = '$delta'
		node_condition_enabled = true   // default false
		separation_of_pc_disjunction = false
		check_pathcondition_satisfiability = true
		constraint_solver = 'CVC4'  // Z3
	] // end symbex
	console [
		verbose = 'MINIMUM'
	] // end console
	shell [
		// Stop stop the current execution if it detects the creation of the above file !
		stop = "symbex.stop"
	] // end shell
}

//EOF of @sew< workflow , 1.0 >:

/*
# Grammar Reference

## Trace Specification
- [*] , use for ANY element
- com_element_id ::= <port_name_id> | <signal_name_id>
- com = <com_element_id>
- input = <com_element_id>
- output = <com_element_id>
- input#env = <com_element_id>
- output#env = <com_element_id>

- variable = <variable_name_id>
- newfresh = <variable_name_id>
- state = <state_name_id>
- transition = <transition_name_id>
- statemachine = <statemachine_name_id>


## Trace Format Specification
- line#wrap#width = 80
- line#wrap#separator = "\n\	"

// %1% --> ec#id
// %2% --> ec#eval
// %3% --> ec#hight
// %4% --> ec#width
// %5% --> ec#weight
// %6% --> statemachine configuration i.e. control node
- context#ufid = "ctx< %1% > %6%"

// %1% --> trace number
// %2% --> execution context leaf identifier
- file#header = "TRACE NUMBER %1%"
- file#begin  = ""
- file#end    = ""

// %1% --> trace number
// %2% --> execution context leaf identifier
- testcase#header = "TRACE NUMBER %1%"
- testcase#begin  = ""
- testcase#end    = ""
- testcase#end    = ""
- init#begin = "\t// Initialization parameter values:"
- init#end   = "\n"

// %1% --> string message
// %2% --> execution context identifier
- comment   = "//%1%"
- separator = "%1%"
- newline   = "\n%1%"

// %1% --> step identifier
// %2% --> execution context identifier
- step#begin = "\t#step#begin %1%"
- step#end   = "\t#step#end %1%"

// %1% --> condition
// %2% --> execution context identifier
- path#condition = "\tPC: %1%"
- path#timed#condition = "\tPtC: %1%"
- node#condition = "\tNC: %1%"
- node#timed#condition = "\tNtC: %1%"

// %1% --> machine runtime pid
// %2% --> machine container identifier
// %3% --> port | signal | variable | machine | transition | routine
// %4% --> value
- time   = "\t%4%"
- assign = "\t%2%:%3% = %4%"
- newfresh = "\tnewfresh %2%->%3%( %4% )"
- input  = "\tinput  %2%->%3%%4%"
- output = "\toutput %2%->%3%%4%"
- input#env  = "\tINPUT  %2%->%3%%4%"
- output#env = "\tOUTPUT %2%->%3%%4%"

*/
