search

verivital / hyst

HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models
http://verivital.com/hyst/
Other
15 stars 18 forks source link

Multi-line init loc() statements not allowed in .cfg #39

Open stanleybak opened 7 years ago

stanleybak commented 7 years ago

SpaceEx is pretty lenient, allowing multi-line init states. We should either parse this correctly or print a better error ("the mismatched quotes on the first line could be a giveaway.").

initially = "loc(CM1_1)==waiting & loc(CM2_1)==waiting & loc(SM1_1)==work & loc(SM2_1)==work & loc(SM3_1)==work & 
loc(SM4_1)==work & loc(SM5_1)==work & loc(SM6_1)==work & loc(SM7_1)==work & 
loc(SM8_1)==work & loc(SM9_1)==work &
loc(Resetter_1)==pre & loc(Time_1)==timing & x_CM1==0 &
CM1 ==0 & CM2 ==0 & SM3_x==0 & t==0 & max_drift ==0.001 & delay == 20 &-max_drift <=drift<=max_drift "
forbidden = "SM3_x >= SM3_x + 2*max_drift"