MenShen:Systematically Ensuring The Confidence of Real Time Home Automaton IoT Systems
Introduction Download Case Studies User Studies

ISY


Rules:


IF SunDetector_0006 execute SunSet THEN Light_0010 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0011 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0012 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0013 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0014 execute OPEN

IF Clock_0001 t==1210 THEN Light_0020 execute OPEN

IF Clock_0001 t==1210 THEN Light_0021 execute OPEN

IF Clock_0002 t==1210 THEN Light_0022 execute OPEN

IF Clock_0002 t==1210 THEN Light_0023 execute OPEN

IF Clock_0003 t==1210 THEN Light_0024 execute OPEN

IF Clock_0003 t==1210 THEN Light_0025 execute OPEN

IF Clock_0004 t==1210 THEN Light_0026 execute OPEN

IF Clock_0004 t==1210 THEN Light_0027 execute OPEN

IF Clock_0005 t==1210 THEN Light_0028 execute OPEN

IF Clock_0005 t==1210 THEN Light_0029 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0030 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0031 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0032 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0033 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0034 execute OPEN

IF SunDetector_0006 execute SunRise THEN Light_0030 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0031 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0032 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0033 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0034 execute CLOSE

IF SunDetector_0006 execute SunSet THEN Light_0040 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0041 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0042 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0043 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0044 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0045 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0046 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0047 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0048 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0049 execute OPEN

IF SunDetector_0006 execute SunRise THEN Light_0040 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0041 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0042 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0043 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0044 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0045 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0046 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0047 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0048 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0049 execute CLOSE

IF SunDetector_0006 execute SunSet THEN Light_0050 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0051 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0052 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0053 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0054 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0055 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0056 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0057 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0058 execute OPEN

IF SunDetector_0006 execute SunSet THEN Light_0059 execute OPEN

IF SunDetector_0006 execute SunRise THEN Light_0050 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0051 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0052 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0053 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0054 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0055 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0056 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0057 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0058 execute CLOSE

IF SunDetector_0006 execute SunRise THEN Light_0059 execute CLOSE


Policy:


The lighe should be on when the time is 20:10.

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 


©2017 SEG, Nanjing University