smg
                    
            player att
              attacker1 ,
	[L_t2_RULE_12__local_DOS_t2_],
	[L_t6_RULE_15__local_exploit_t6_],
	[L_t8_RULE_15__local_exploit_t8_],
	[L_t10_RULE_16__remote_exploit_of_a_server_progt10_],
	[L_t12_RULE_19__multi_hop_access_t12_],
	[L_t14_RULE_19__multi_hop_access_t14_],
	[L_t15_RULE_19__multi_hop_access_t15_],
	[L_t18_RULE_15__local_exploit_t18_],
	[L_t20_RULE_9__Tampering_the_code_memory_t20_],
	[L_t22_RULE_22__Access_a_host_through_executingt22_],
	[L_t23_RULE_23__Access_a_host_through_a_log_in_t23_],
	[L_t25_RULE_19__multi_hop_access_t25_],
	[L_t27_RULE_19__multi_hop_access_t27_],
	[L_t28_RULE_19__multi_hop_access_t28_],
	[L_t30_RULE_19__multi_hop_access_t30_],
	[L_t33_RULE_15__local_exploit_t33_],
	[L_t35_RULE_15__local_exploit_t35_],
	[L_t37_RULE_16__remote_exploit_of_a_server_progt37_],
	[L_t39_RULE_19__multi_hop_access_t39_],
	[L_t41_RULE_19__multi_hop_access_t41_],
	[L_t42_RULE_19__multi_hop_access_t42_],
	[L_t44_RULE_19__multi_hop_access_t44_],
	[L_t46_RULE_19__multi_hop_access_t46_],
	[L_t49_RULE_9__Tampering_the_code_memory_t49_],
	[L_t51_RULE_22__Access_a_host_through_executingt51_],
	[L_t52_RULE_22__Access_a_host_through_executingt52_],
	[L_t53_RULE_23__Access_a_host_through_a_log_in_t53_],
	[L_t55_RULE_27__remote_ssh_to_a_host_t55_],
	[L_t58_RULE_9__Tampering_the_code_memory_t58_],
	[L_t60_RULE_19__multi_hop_access_t60_],
	[L_t61_RULE_20__direct_network_access_t61_],
	[L_t65_RULE_27__remote_ssh_to_a_host_t65_],
	[L_t69_RULE_19__multi_hop_access_t69_],
	[L_t71_RULE_19__multi_hop_access_t71_],
	[L_t72_RULE_20__direct_network_access_t72_],
	[L_t76_RULE_9__Tampering_the_code_memory_t76_],
	[L_t78_RULE_22__Access_a_host_through_executingt78_],
	[L_t79_RULE_22__Access_a_host_through_executingt79_],
	[L_t80_RULE_23__Access_a_host_through_a_log_in_t80_],
	[L_t82_RULE_27__remote_ssh_to_a_host_t82_],
	[L_t85_RULE_12__local_DOS_t85_],
	[L_t86_RULE_12__local_DOS_t86_],
	[L_t89_RULE_12__local_DOS_t89_],
	[L_t90_RULE_13__remote_DOS_on_a_server_program_t90_],
	[L_t93_RULE_13__remote_DOS_on_a_server_program_t93_],
	[L_t97_RULE_1__System_is_compromised_t97_],
	[L_t99_RULE_6__Leaking_data_information_due_to_t99_],
	[L_t101_RULE_6__Leaking_data_information_due_to_t101_],
	[L_t102_RULE_6__Leaking_data_information_due_to_t102_],
	[L_t104_RULE_6__Leaking_data_information_due_to_t104_],
	[L_t105_RULE_1__System_is_compromised_t105_],
	[L_t107_RULE_5__Leaking_file_information_due_to_t107_],
	[L_t109_RULE_5__Leaking_file_information_due_to_t109_],
	[L_t110_RULE_2__System_is_compromised_t110_],
	[L_t111_RULE_3__System_is_compromised_t111_],
	[L_t113_RULE_7__Tamering_data_due_to_a_vulnerabit113_],
	[L_t115_RULE_7__Tamering_data_due_to_a_vulnerabit115_],
	[L_t116_RULE_3__System_is_compromised_t116_],
	[L_t118_RULE_7__Tamering_data_due_to_a_vulnerabit118_],
	[L_t121_RULE_7__Tamering_data_due_to_a_vulnerabit121_]
            endplayer 
            
            player def
              defender ,
	[def_L_t6_RULE_15__local_exploit_t6_ ],
	[def_L_t10_RULE_16__remote_exploit_of_a_server_progt10_ ],
	[def_L_t12_RULE_19__multi_hop_access_t12_ ],
	[def_L_t18_RULE_15__local_exploit_t18_ ],
	[def_L_t20_RULE_9__Tampering_the_code_memory_t20_ ],
	[def_L_t25_RULE_19__multi_hop_access_t25_ ],
	[def_L_t53_RULE_23__Access_a_host_through_a_log_in_t53_ ],
	[def_L_t76_RULE_9__Tampering_the_code_memory_t76_ ]
            endplayer
            
                 global dos_plycent02_ : bool init false;
     global misuseAction_overusecpu_ : bool init true;
     global vulExists_plycent02__cve_2018_8897___cen : bool init true;
     global execCode_plycent02_root_ : bool init false;
     global vulExists_plycent02__cve_2017_9076___cen : bool init true;
     global execCode_plycent02_user_ : bool init false;
     global netAccess_plycent02_tcp_22_ : bool init false;
     global hacl_plycent02_plycent02_tcp_22_ : bool init true;
     global hacl_plycent03_plycent02_tcp_22_ : bool init true;
     global execCode_plycent03_root_ : bool init false;
     global vulExists_plycent03__cve_2017_16939___ce : bool init true;
     global canAccessHost_plycent03_ : bool init false;
     global netAccess_plycent03_tcp_22_ : bool init false;
     global hacl_plycent02_plycent03_tcp_22_ : bool init true;
     global hacl_plycent03_plycent03_tcp_22_ : bool init true;
     global hacl_plyrhel01_plycent03_tcp_22_ : bool init true;
     global execCode_plyrhel01_root_ : bool init false;
     global vulExists_plyrhel01__cve_2017_16939___re : bool init true;
     global execCode_plyrhel01_user_ : bool init false;
     global netAccess_plyrhel01_tcp_22_ : bool init false;
     global hacl_plycent02_plyrhel01_tcp_22_ : bool init true;
     global hacl_plycent03_plyrhel01_tcp_22_ : bool init true;
     global hacl_plyrhel01_plyrhel01_tcp_22_ : bool init true;
     global networkServiceInfo_plyrhel01__redhatente : bool init true;
     global vulExists_plyrhel01__cve_2017_16997___re : bool init true;
     global canAccessHost_plyrhel01_ : bool init false;
     global logInService_plyrhel01_tcp_22_ : bool init false;
     global sshDaemon__redhatenterpriselinux7_5__ : bool init true;
     global vulExists_plyrhel01__cve_2018_3136___red : bool init true;
     global vulExists_plyrhel01__cve_2018_7566___red : bool init true;
     global hacl_internet_plycent03_tcp_22_ : bool init true;
     global attackerLocated_internet_ : bool init true;
     global logInService_plycent03_tcp_22_ : bool init false;
     global sshDaemon__centos7_5_1804__ : bool init true;
     global networkServiceInfo_plycent03__centos7_5_ : bool init true;
     global vulExists_plycent03__cve_2018_7566___cen : bool init true;
     global hacl_plyrhel01_plycent02_tcp_22_ : bool init true;
     global hacl_internet_plycent02_tcp_22_ : bool init true;
     global networkServiceInfo_plycent02__centos6_10 : bool init true;
     global vulExists_plycent02__cve_2018_1000004___ : bool init true;
     global canAccessHost_plycent02_ : bool init false;
     global logInService_plycent02_tcp_22_ : bool init false;
     global sshDaemon__centos6_10__ : bool init true;
     global vulExists_plycent02__cve_2018_7566___cen : bool init true;
     global misuseAction_overusememory_ : bool init true;
     global scoreCvss_59__cve_2018_1000004__ : bool init true;
     global scoreCvss_75__cve_2018_5390__ : bool init true;
     global vulExists_plycent02__cve_2018_5390___cen : bool init true;
     global systemDown_plycent02_ : bool init false;
     global leakInfo_plycent02_data_ : bool init false;
     global vulExists_plycent02__cve_2017_1000410___ : bool init true;
     global vulExists_plycent02__cve_2017_7889___cen : bool init true;
     global leakInfo_plycent02_file_ : bool init false;
     global vulExists_plycent02__cve_2017_7616___cen : bool init true;
     global tamperInfo_plycent02_code_ : bool init false;
     global modifyInfoAct_writecode_code_ : bool init true;
     global tamperInfo_plycent02_data_ : bool init false;
     global modifyInfoAct_writedata_data_ : bool init true;

     global t : [1..3] init 1; // the players turn 

            
            module attacker1
            
	[L_t2_RULE_12__local_DOS_t2_] misuseAction_overusecpu_ &
			 vulExists_plycent02__cve_2018_8897___cen &
			 execCode_plycent02_root_ &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.768: (dos_plycent02_' = true)   & (t'=1) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t6_RULE_15__local_exploit_t6_] execCode_plycent02_root_ &
			 vulExists_plycent02__cve_2017_9076___cen &
			 !execCode_plycent02_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plycent02_root_' = true)   & (t'=2) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t8_RULE_15__local_exploit_t8_] vulExists_plycent02__cve_2017_9076___cen &
			 execCode_plycent02_user_ &
			 !execCode_plycent02_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plycent02_root_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t10_RULE_16__remote_exploit_of_a_server_progt10_] netAccess_plycent02_tcp_22_ &
			 networkServiceInfo_plycent02__centos6_10 &
			 vulExists_plycent02__cve_2018_1000004___ &
			 !execCode_plycent02_user_ & !dos_plycent02_ & (t=1) -> 
				0.7979: (execCode_plycent02_user_' = true)   & (t'=2) +0.1347333333333333: (t'=1) +0.06736666666666664: (t'=3);

	[L_t12_RULE_19__multi_hop_access_t12_] execCode_plycent02_root_ &
			 hacl_plycent02_plycent02_tcp_22_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.768: (netAccess_plycent02_tcp_22_' = true)   & (t'=2) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t14_RULE_19__multi_hop_access_t14_] execCode_plycent02_user_ &
			 hacl_plycent02_plycent02_tcp_22_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent02_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t15_RULE_19__multi_hop_access_t15_] hacl_plycent03_plycent02_tcp_22_ &
			 execCode_plycent03_root_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.7219: (netAccess_plycent02_tcp_22_' = true)   & (t'=1) +0.1854: (t'=1) +0.0927: (t'=3);

	[L_t18_RULE_15__local_exploit_t18_] execCode_plycent03_root_ &
			 vulExists_plycent03__cve_2017_16939___ce &
			 !execCode_plycent03_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plycent03_root_' = true)   & (t'=2) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t20_RULE_9__Tampering_the_code_memory_t20_] canAccessHost_plycent03_ &
			 vulExists_plycent03__cve_2018_7566___cen &
			 !execCode_plycent03_root_ & !dos_plycent02_ & (t=1) -> 
				0.5118: (execCode_plycent03_root_' = true)   & (t'=2) +0.3254666666666666: (t'=1) +0.1627333333333333: (t'=3);

	[L_t22_RULE_22__Access_a_host_through_executingt22_] execCode_plycent03_root_ &
			 !canAccessHost_plycent03_ & !dos_plycent02_ & (t=1) -> 
				0.7219: (canAccessHost_plycent03_' = true)   & (t'=1) +0.1854: (t'=1) +0.0927: (t'=3);

	[L_t23_RULE_23__Access_a_host_through_a_log_in_t23_] netAccess_plycent03_tcp_22_ &
			 logInService_plycent03_tcp_22_ &
			 !canAccessHost_plycent03_ & !dos_plycent02_ & (t=1) -> 
				0.6398: (canAccessHost_plycent03_' = true)   & (t'=1) +0.2401333333333333: (t'=1) +0.12006666666666665: (t'=3);

	[L_t25_RULE_19__multi_hop_access_t25_] execCode_plycent02_root_ &
			 hacl_plycent02_plycent03_tcp_22_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent03_tcp_22_' = true)   & (t'=2) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t27_RULE_19__multi_hop_access_t27_] execCode_plycent02_user_ &
			 hacl_plycent02_plycent03_tcp_22_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent03_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t28_RULE_19__multi_hop_access_t28_] execCode_plycent03_root_ &
			 hacl_plycent03_plycent03_tcp_22_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent03_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t30_RULE_19__multi_hop_access_t30_] hacl_plyrhel01_plycent03_tcp_22_ &
			 execCode_plyrhel01_root_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.7969: (netAccess_plycent03_tcp_22_' = true)   & (t'=1) +0.13539999999999996: (t'=1) +0.06769999999999998: (t'=3);

	[L_t33_RULE_15__local_exploit_t33_] execCode_plyrhel01_root_ &
			 vulExists_plyrhel01__cve_2017_16939___re &
			 !execCode_plyrhel01_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plyrhel01_root_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t35_RULE_15__local_exploit_t35_] vulExists_plyrhel01__cve_2017_16939___re &
			 execCode_plyrhel01_user_ &
			 !execCode_plyrhel01_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plyrhel01_root_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t37_RULE_16__remote_exploit_of_a_server_progt37_] netAccess_plyrhel01_tcp_22_ &
			 networkServiceInfo_plyrhel01__redhatente &
			 vulExists_plyrhel01__cve_2017_16997___re &
			 !execCode_plyrhel01_user_ & !dos_plycent02_ & (t=1) -> 
				0.7997: (execCode_plyrhel01_user_' = true)   & (t'=1) +0.13353333333333336: (t'=1) +0.06676666666666668: (t'=3);

	[L_t39_RULE_19__multi_hop_access_t39_] execCode_plycent02_root_ &
			 hacl_plycent02_plyrhel01_tcp_22_ &
			 !netAccess_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t41_RULE_19__multi_hop_access_t41_] execCode_plycent02_user_ &
			 hacl_plycent02_plyrhel01_tcp_22_ &
			 !netAccess_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t42_RULE_19__multi_hop_access_t42_] execCode_plycent03_root_ &
			 hacl_plycent03_plyrhel01_tcp_22_ &
			 !netAccess_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t44_RULE_19__multi_hop_access_t44_] execCode_plyrhel01_root_ &
			 hacl_plyrhel01_plyrhel01_tcp_22_ &
			 !netAccess_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t46_RULE_19__multi_hop_access_t46_] execCode_plyrhel01_user_ &
			 hacl_plyrhel01_plyrhel01_tcp_22_ &
			 !netAccess_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t49_RULE_9__Tampering_the_code_memory_t49_] canAccessHost_plyrhel01_ &
			 vulExists_plyrhel01__cve_2018_3136___red &
			 !execCode_plyrhel01_root_ & !dos_plycent02_ & (t=1) -> 
				0.512: (execCode_plyrhel01_root_' = true)   & (t'=1) +0.3253333333333333: (t'=1) +0.16266666666666665: (t'=3);

	[L_t51_RULE_22__Access_a_host_through_executingt51_] execCode_plyrhel01_root_ &
			 !canAccessHost_plyrhel01_ & !dos_plycent02_ & (t=1) -> 
				0.7969: (canAccessHost_plyrhel01_' = true)   & (t'=1) +0.13539999999999996: (t'=1) +0.06769999999999998: (t'=3);

	[L_t52_RULE_22__Access_a_host_through_executingt52_] execCode_plyrhel01_user_ &
			 !canAccessHost_plyrhel01_ & !dos_plycent02_ & (t=1) -> 
				0.6398: (canAccessHost_plyrhel01_' = true)   & (t'=1) +0.2401333333333333: (t'=1) +0.12006666666666665: (t'=3);

	[L_t53_RULE_23__Access_a_host_through_a_log_in_t53_] netAccess_plyrhel01_tcp_22_ &
			 logInService_plyrhel01_tcp_22_ &
			 !canAccessHost_plyrhel01_ & !dos_plycent02_ & (t=1) -> 
				0.64: (canAccessHost_plyrhel01_' = true)   & (t'=2) +0.24: (t'=1) +0.12: (t'=3);

	[L_t55_RULE_27__remote_ssh_to_a_host_t55_] networkServiceInfo_plyrhel01__redhatente &
			 sshDaemon__redhatenterpriselinux7_5__ &
			 !logInService_plyrhel01_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (logInService_plyrhel01_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t58_RULE_9__Tampering_the_code_memory_t58_] canAccessHost_plyrhel01_ &
			 vulExists_plyrhel01__cve_2018_7566___red &
			 !execCode_plyrhel01_root_ & !dos_plycent02_ & (t=1) -> 
				0.8: (execCode_plyrhel01_root_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t60_RULE_19__multi_hop_access_t60_] hacl_plyrhel01_plycent03_tcp_22_ &
			 execCode_plyrhel01_user_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent03_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t61_RULE_20__direct_network_access_t61_] hacl_internet_plycent03_tcp_22_ &
			 attackerLocated_internet_ &
			 !netAccess_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent03_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t65_RULE_27__remote_ssh_to_a_host_t65_] sshDaemon__centos7_5_1804__ &
			 networkServiceInfo_plycent03__centos7_5_ &
			 !logInService_plycent03_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (logInService_plycent03_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t69_RULE_19__multi_hop_access_t69_] execCode_plyrhel01_root_ &
			 hacl_plyrhel01_plycent02_tcp_22_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.7969: (netAccess_plycent02_tcp_22_' = true)   & (t'=1) +0.13539999999999996: (t'=1) +0.06769999999999998: (t'=3);

	[L_t71_RULE_19__multi_hop_access_t71_] execCode_plyrhel01_user_ &
			 hacl_plyrhel01_plycent02_tcp_22_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent02_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t72_RULE_20__direct_network_access_t72_] attackerLocated_internet_ &
			 hacl_internet_plycent02_tcp_22_ &
			 !netAccess_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (netAccess_plycent02_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t76_RULE_9__Tampering_the_code_memory_t76_] canAccessHost_plycent02_ &
			 vulExists_plycent02__cve_2018_7566___cen &
			 !execCode_plycent02_root_ & !dos_plycent02_ & (t=1) -> 
				0.512: (execCode_plycent02_root_' = true)   & (t'=2) +0.3253333333333333: (t'=1) +0.16266666666666665: (t'=3);

	[L_t78_RULE_22__Access_a_host_through_executingt78_] execCode_plycent02_root_ &
			 !canAccessHost_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.768: (canAccessHost_plycent02_' = true)   & (t'=1) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t79_RULE_22__Access_a_host_through_executingt79_] execCode_plycent02_user_ &
			 !canAccessHost_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.6383: (canAccessHost_plycent02_' = true)   & (t'=1) +0.24113333333333334: (t'=1) +0.12056666666666667: (t'=3);

	[L_t80_RULE_23__Access_a_host_through_a_log_in_t80_] netAccess_plycent02_tcp_22_ &
			 logInService_plycent02_tcp_22_ &
			 !canAccessHost_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.64: (canAccessHost_plycent02_' = true)   & (t'=1) +0.24: (t'=1) +0.12: (t'=3);

	[L_t82_RULE_27__remote_ssh_to_a_host_t82_] networkServiceInfo_plycent02__centos6_10 &
			 sshDaemon__centos6_10__ &
			 !logInService_plycent02_tcp_22_ & !dos_plycent02_ & (t=1) -> 
				0.8: (logInService_plycent02_tcp_22_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t85_RULE_12__local_DOS_t85_] misuseAction_overusecpu_ &
			 vulExists_plycent02__cve_2018_8897___cen &
			 execCode_plycent02_user_ &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.8: (dos_plycent02_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t86_RULE_12__local_DOS_t86_] execCode_plycent02_root_ &
			 misuseAction_overusememory_ &
			 vulExists_plycent02__cve_2017_9076___cen &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.8: (dos_plycent02_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t89_RULE_12__local_DOS_t89_] execCode_plycent02_user_ &
			 misuseAction_overusememory_ &
			 vulExists_plycent02__cve_2017_9076___cen &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.8: (dos_plycent02_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t90_RULE_13__remote_DOS_on_a_server_program_t90_] netAccess_plycent02_tcp_22_ &
			 networkServiceInfo_plycent02__centos6_10 &
			 misuseAction_overusememory_ &
			 scoreCvss_59__cve_2018_1000004__ &
			 vulExists_plycent02__cve_2018_1000004___ &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.8: (dos_plycent02_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t93_RULE_13__remote_DOS_on_a_server_program_t93_] misuseAction_overusecpu_ &
			 netAccess_plycent02_tcp_22_ &
			 networkServiceInfo_plycent02__centos6_10 &
			 scoreCvss_75__cve_2018_5390__ &
			 vulExists_plycent02__cve_2018_5390___cen &
			 !dos_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.8: (dos_plycent02_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t97_RULE_1__System_is_compromised_t97_] leakInfo_plycent02_data_ &
			 !systemDown_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.7987: (systemDown_plycent02_' = true)   & (t'=1) +0.1342: (t'=1) +0.0671: (t'=3);

	[L_t99_RULE_6__Leaking_data_information_due_to_t99_] execCode_plycent02_root_ &
			 vulExists_plycent02__cve_2017_1000410___ &
			 !leakInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t101_RULE_6__Leaking_data_information_due_to_t101_] execCode_plycent02_user_ &
			 vulExists_plycent02__cve_2017_1000410___ &
			 !leakInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t102_RULE_6__Leaking_data_information_due_to_t102_] execCode_plycent02_root_ &
			 vulExists_plycent02__cve_2017_7889___cen &
			 !leakInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t104_RULE_6__Leaking_data_information_due_to_t104_] execCode_plycent02_user_ &
			 vulExists_plycent02__cve_2017_7889___cen &
			 !leakInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t105_RULE_1__System_is_compromised_t105_] leakInfo_plycent02_file_ &
			 !systemDown_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.768: (systemDown_plycent02_' = true)   & (t'=1) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t107_RULE_5__Leaking_file_information_due_to_t107_] execCode_plycent02_root_ &
			 vulExists_plycent02__cve_2017_7616___cen &
			 !leakInfo_plycent02_file_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_file_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t109_RULE_5__Leaking_file_information_due_to_t109_] execCode_plycent02_user_ &
			 vulExists_plycent02__cve_2017_7616___cen &
			 !leakInfo_plycent02_file_ & !dos_plycent02_ & (t=1) -> 
				0.8: (leakInfo_plycent02_file_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t110_RULE_2__System_is_compromised_t110_] dos_plycent02_ &
			 !systemDown_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.7999: (systemDown_plycent02_' = true)   & (t'=1) +0.13339999999999996: (t'=1) +0.06669999999999998: (t'=3);

	[L_t111_RULE_3__System_is_compromised_t111_] tamperInfo_plycent02_code_ &
			 !systemDown_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.768: (systemDown_plycent02_' = true)   & (t'=1) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t113_RULE_7__Tamering_data_due_to_a_vulnerabit113_] execCode_plycent02_root_ &
			 vulExists_plycent02__cve_2018_7566___cen &
			 modifyInfoAct_writecode_code_ &
			 !tamperInfo_plycent02_code_ & !dos_plycent02_ & (t=1) -> 
				0.8: (tamperInfo_plycent02_code_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t115_RULE_7__Tamering_data_due_to_a_vulnerabit115_] execCode_plycent02_user_ &
			 vulExists_plycent02__cve_2018_7566___cen &
			 modifyInfoAct_writecode_code_ &
			 !tamperInfo_plycent02_code_ & !dos_plycent02_ & (t=1) -> 
				0.8: (tamperInfo_plycent02_code_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t116_RULE_3__System_is_compromised_t116_] tamperInfo_plycent02_data_ &
			 !systemDown_plycent02_ & !dos_plycent02_ & (t=1) -> 
				0.768: (systemDown_plycent02_' = true)   & (t'=1) +0.15466666666666665: (t'=1) +0.07733333333333332: (t'=3);

	[L_t118_RULE_7__Tamering_data_due_to_a_vulnerabit118_] execCode_plycent02_root_ &
			 modifyInfoAct_writedata_data_ &
			 vulExists_plycent02__cve_2017_7889___cen &
			 !tamperInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (tamperInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

	[L_t121_RULE_7__Tamering_data_due_to_a_vulnerabit121_] execCode_plycent02_user_ &
			 modifyInfoAct_writedata_data_ &
			 vulExists_plycent02__cve_2017_7889___cen &
			 !tamperInfo_plycent02_data_ & !dos_plycent02_ & (t=1) -> 
				0.8: (tamperInfo_plycent02_data_' = true)   & (t'=1) +0.1333333333333333: (t'=1) +0.06666666666666665: (t'=3);

            endmodule
            
            
            
            module defender
            
            	[def_L_t6_RULE_15__local_exploit_t6_ ] execCode_plycent02_root_ & (t=2) -> 
			 0.6: (networkServiceInfo_plycent02__centos6_10' = false) & (vulExists_plycent02__cve_2018_1000004___' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t10_RULE_16__remote_exploit_of_a_server_progt10_ ] execCode_plycent02_user_ & (t=2) -> 
			 0.6: (misuseAction_overusecpu_' = false) & (vulExists_plycent02__cve_2018_8897___cen' = false) & (misuseAction_overusememory_' = false) & (vulExists_plycent02__cve_2017_9076___cen' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t12_RULE_19__multi_hop_access_t12_ ] netAccess_plycent02_tcp_22_ & (t=2) -> 
			 0.6: (misuseAction_overusecpu_' = false) & (vulExists_plycent02__cve_2018_8897___cen' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t18_RULE_15__local_exploit_t18_ ] execCode_plycent03_root_ & (t=2) -> 
			 0.6: (networkServiceInfo_plycent02__centos6_10' = false) & (misuseAction_overusememory_' = false) & (scoreCvss_59__cve_2018_1000004__' = false) & (vulExists_plycent02__cve_2018_1000004___' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t20_RULE_9__Tampering_the_code_memory_t20_ ] execCode_plycent03_root_ & (t=2) -> 
			 0.6: (hacl_plycent03_plycent02_tcp_22_' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t25_RULE_19__multi_hop_access_t25_ ] netAccess_plycent03_tcp_22_ & (t=2) -> 
			 0.6: (vulExists_plycent02__cve_2017_9076___cen' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t53_RULE_23__Access_a_host_through_a_log_in_t53_ ] canAccessHost_plyrhel01_ & (t=2) -> 
			 0.6: (vulExists_plyrhel01__cve_2017_16939___re' = false) & (t'=1)  + 0.4: (t'=1);
	[def_L_t76_RULE_9__Tampering_the_code_memory_t76_ ] execCode_plycent02_root_ & (t=2) -> 
			 0.6: (misuseAction_overusecpu_' = false) & (vulExists_plycent02__cve_2018_8897___cen' = false) & (t'=1)  + 0.4: (t'=1);

 endmodule