add the shift operators
add way to model check NuSMV output