add "event" in state's small-step semantics
add "trace" to configuration
let writes/reads depend on events; redefine stuck of state
add SC semantics
try defining DRF Property
change name to st_normal_form & cfg_normal_form
Merge branch 'drf' into dev

Conflicts:
	tso.v