// Description:  Simplified PC configuration example
// Author:  CLab# Crew
// Date:  2006-08-21

type
CpuSlot{Slot1,Socket7,SuperSocket7,SlotA};
Slot{PCI,ISA,AGP,NONE};
RamSlot{SDRAM168Pin,Std72Pin,EDO72Pin};
HdBus{IDE,SCSI_UW2,SSCI_2};
HdCapacity{R0Gb,R10Gb,R31Gb,R36Gb};
CpuFreq{"P500MHz","P600MHz","P700MHz","P800MHz"};
RamCapacity[0..4];//256,2=512 3=768 4 = 1024 MB ram

MotherboardId
{
	Asus_K7M_ATX,
	Microstar_6167_ATX,
	Aopen_AK_72_133_ATX};

ProcessorId
	{"AMDAthlonP800MHz"
	,"AMDAthlonP500MHz"
	,"IntelPentiumIIIP600MHz"
	};
HarddiskId	{"Noharddisk"
	,"QuantumAtlasIV36_4GB"
	,"MaxtorDiamondMax40pluss30_7GB"
	,"IBMDeskStar25GP10_1GB"
	};
RamId
	{"NoRAMBlock"
	,"SDRAMPC100NONAME256MB"
	,"SDRAMPC533512MB"
	};


GraphicsCardId
	{"AsusAGPV3400TNTmTVInTVOut"
	,"DiamondViper770"
	,"CreativeLabsGraphicsBlasterRivaTNT"
	};
RamExist[0..1];
slotcount[0..4];
ramblockCount[0..4];
controllerCount[0..4];

variable


//private vars, placed first due to BDD graph efficience with this variable ordering
MotherboardId MOTHERBOARD; //1

CpuSlot priv_motherbrdCpuslot;//23

HdBus priv_motherbrdCtrType;//3
controllerCount priv_motherBrdContrCnt;//24
CpuFreq priv_mincpufreq;//25
CpuFreq priv_maxCpufreq;//26
RamSlot priv_motherbrdRamSlot;//2
ramblockCount priv_ramcap; //0
Slot priv_slotOne; //8
Slot priv_slotTwo; //9
Slot priv_slotThree; //10
Slot priv_slotFour; //11

CpuFreq priv_processoFreq;
CpuSlot priv_processorCpuSlot;



//public config-variables
CpuFreq PC_CLOCK;//11
RamCapacity PC_RAM_CAPACITY; //12
ProcessorId PROCESSOR; //6
HarddiskId HARDDISK1; //7
HdCapacity HARDDISK1_CAPACITY; //8
HarddiskId HARDDISK2; //9
HdCapacity HARDDISK2_CAPACITY; // 10
RamId RAM1; //4
RamId RAM2; //5
RamId RAM3; //6
RamId RAM4; //7
GraphicsCardId GRAPHIC_CARD;


//private variables:




Slot priv_graphiccrdSlot;//27
HdBus priv_harddisk1Bus;
HdBus priv_harddisk2Bus;
RamSlot priv_ram1Slot;
RamCapacity priv_ram1Cap;
RamExist priv_ram1Exist;
RamSlot priv_ram2Slot;
RamCapacity priv_ram2Cap;
RamExist priv_ram2Exist;
RamSlot priv_ram3Slot;
RamCapacity priv_ram3Cap;
RamExist priv_ram3Exist;
RamSlot priv_ram4Slot;
RamCapacity priv_ram4Cap;
RamExist priv_ram4Exist;



rule
	(((MOTHERBOARD==Asus_K7M_ATX)&&(priv_motherbrdCpuslot==SlotA&&priv_motherbrdCtrType==IDE
		&&priv_motherBrdContrCnt==4&&priv_mincpufreq=="P500MHz"
		&&priv_maxCpufreq=="P700MHz"&&priv_motherbrdRamSlot==SDRAM168Pin
		&&priv_ramcap==3&&priv_slotOne==PCI
		&&priv_slotTwo==PCI&&priv_slotThree==AGP
		&&priv_slotFour==PCI))

	||
	((MOTHERBOARD==Microstar_6167_ATX)&&(priv_motherbrdCpuslot==SlotA
		&&priv_motherbrdCtrType==IDE&&priv_motherBrdContrCnt==4
		&&priv_mincpufreq=="P500MHz"&&priv_maxCpufreq=="P700MHz"
		&&priv_motherbrdRamSlot==SDRAM168Pin&&priv_ramcap==3
		&&priv_slotOne==PCI&&priv_slotTwo==PCI
		&&priv_slotThree==PCI&&priv_slotFour==AGP
	))
	||
	((MOTHERBOARD==Aopen_AK_72_133_ATX)&&(priv_motherbrdCpuslot==SlotA
		&&priv_motherbrdCtrType==IDE&&priv_motherBrdContrCnt==4
		&&priv_mincpufreq=="P500MHz"&&priv_maxCpufreq=="P800MHz"
		&&priv_motherbrdRamSlot==SDRAM168Pin&&priv_ramcap==3
		&&priv_slotOne==PCI&&priv_slotTwo==PCI
		&&priv_slotThree==PCI&&priv_slotFour==AGP
		))

);

//making cpu slots match between cpu and motherboard:
(((priv_motherbrdCpuslot==Slot1)&&(priv_processorCpuSlot==Slot1)) ||
((priv_motherbrdCpuslot==Socket7)&&(priv_processorCpuSlot==Socket7)) ||
((priv_motherbrdCpuslot==SuperSocket7)&&(priv_processorCpuSlot==SuperSocket7)) ||
((priv_motherbrdCpuslot==SlotA)&&(priv_processorCpuSlot==SlotA)));


//orignal processorrules:
		((PROCESSOR=="AMDAthlonP800MHz"&&priv_processorCpuSlot==SlotA
			&&priv_processoFreq=="P800MHz")
		||
		(PROCESSOR=="AMDAthlonP500MHz"&&priv_processorCpuSlot==SlotA
			&&priv_processoFreq=="P500MHz")
		||
		(PROCESSOR=="IntelPentiumIIIP600MHz"&&priv_processorCpuSlot==Slot1
			&&priv_processoFreq=="P600MHz"));
			
//making ram slots match between ram and motherboard:
(((priv_motherbrdRamSlot==Std72Pin)&&((priv_ram1Slot==Std72Pin)&&(priv_ram2Slot==Std72Pin)&&(priv_ram3Slot==Std72Pin)&&(priv_ram4Slot==Std72Pin))) ||
((priv_motherbrdRamSlot==EDO72Pin)&&((priv_ram1Slot==EDO72Pin)&&(priv_ram2Slot==EDO72Pin)&&(priv_ram3Slot==EDO72Pin)&&(priv_ram4Slot==EDO72Pin))) ||
((priv_motherbrdRamSlot==SDRAM168Pin)&&((priv_ram1Slot==SDRAM168Pin)&&(priv_ram2Slot==SDRAM168Pin)&&(priv_ram3Slot==SDRAM168Pin)&&(priv_ram4Slot==SDRAM168Pin))));

//ram rules:
//ram1rules
	(RAM1=="NoRAMBlock"&&priv_ram1Slot==Std72Pin
		&&priv_ram1Cap==0)
	||
	(RAM1=="NoRAMBlock"&&priv_ram1Slot==SDRAM168Pin
		&&priv_ram1Cap==0)
	||
	(RAM1=="SDRAMPC533512MB"&&priv_ram1Slot==SDRAM168Pin
		&&priv_ram1Cap==2)
	||
	(RAM1=="SDRAMPC100NONAME256MB"&&priv_ram1Slot==SDRAM168Pin
		&&priv_ram1Cap==1);


//ram2rules
	(RAM2=="NoRAMBlock"&&priv_ram2Slot==Std72Pin
		&&priv_ram2Cap==0)
	||
	(RAM2=="NoRAMBlock"&&priv_ram2Slot==SDRAM168Pin
		&&priv_ram2Cap==0)
	||
	(RAM2=="SDRAMPC533512MB"&&priv_ram2Slot==SDRAM168Pin
		&&priv_ram2Cap==2)
	||
	(RAM2=="SDRAMPC100NONAME256MB"&&priv_ram2Slot==SDRAM168Pin
		&&priv_ram2Cap==1);


//ram3rules
	(RAM3=="NoRAMBlock"&&priv_ram3Slot==Std72Pin
		&&priv_ram3Cap==0)
	||
	(RAM3=="NoRAMBlock"&&priv_ram3Slot==SDRAM168Pin
		&&priv_ram3Cap==0)
	||
	(RAM3=="SDRAMPC533512MB"&&priv_ram3Slot==SDRAM168Pin
		&&priv_ram3Cap==2)
	||
	(RAM3=="SDRAMPC100NONAME256MB"&&priv_ram3Slot==SDRAM168Pin
		&&priv_ram3Cap==1);

//ram4rules
	(RAM4=="NoRAMBlock" && priv_ram4Slot==Std72Pin
		&&priv_ram4Cap==0)
	||
	(RAM4=="NoRAMBlock" && priv_ram4Slot==SDRAM168Pin
		&&priv_ram4Cap==0)
	||
	(RAM4=="SDRAMPC533512MB" && priv_ram4Slot==SDRAM168Pin
		&&priv_ram4Cap==2)
        ||
	(RAM4=="SDRAMPC100NONAME256MB" && priv_ram4Slot==SDRAM168Pin
		&&priv_ram4Cap==1);

//motherboard-harddisk bindings:
((priv_motherbrdCtrType==IDE)&&(priv_harddisk1Bus==IDE&&priv_harddisk2Bus==IDE) ||
(priv_motherbrdCtrType==SCSI_UW2)&&(priv_harddisk1Bus==SCSI_UW2&&priv_harddisk2Bus==SCSI_UW2) ||
(priv_motherbrdCtrType==SSCI_2)&&(priv_harddisk1Bus==SSCI_2&&priv_harddisk2Bus==SSCI_2));


(HARDDISK1=="Noharddisk"&&priv_harddisk1Bus==IDE
		&&HARDDISK1_CAPACITY==R0Gb)
	||
	(HARDDISK1=="Noharddisk"&&priv_harddisk1Bus==SCSI_UW2
		&&HARDDISK1_CAPACITY==R0Gb)
	||
	(HARDDISK1=="IBMDeskStar25GP10_1GB"&&priv_harddisk1Bus==IDE
		&&HARDDISK1_CAPACITY==R10Gb)
	||
	(HARDDISK1=="MaxtorDiamondMax40pluss30_7GB"&&priv_harddisk1Bus==IDE
		&&HARDDISK1_CAPACITY==R31Gb)
	||
	(HARDDISK1=="QuantumAtlasIV36_4GB"&&priv_harddisk1Bus==SCSI_UW2
		&&HARDDISK1_CAPACITY==R36Gb)
	;

//harddisk rules



	//harddisk2rules
	(HARDDISK2=="Noharddisk"&&priv_harddisk2Bus==IDE
		&&HARDDISK2_CAPACITY==R0Gb)
	||
	(HARDDISK2=="Noharddisk"&&priv_harddisk2Bus==SCSI_UW2
		&&HARDDISK2_CAPACITY==R0Gb)
	||
	(HARDDISK2=="IBMDeskStar25GP10_1GB"&&priv_harddisk2Bus==IDE
		&&HARDDISK2_CAPACITY==R10Gb)
	||
	(HARDDISK2=="MaxtorDiamondMax40pluss30_7GB"&&priv_harddisk2Bus==IDE
		&&HARDDISK2_CAPACITY==R31Gb)
	||
	(HARDDISK2=="QuantumAtlasIV36_4GB"&&priv_harddisk2Bus==SCSI_UW2
		&&HARDDISK2_CAPACITY==R36Gb)
	;


// graphic card slot bindings
(((priv_graphiccrdSlot==NONE)&&((priv_slotOne==NONE)||(priv_slotTwo==NONE)||(priv_slotThree==NONE)||(priv_slotFour==NONE))) ||

	((priv_graphiccrdSlot==PCI)&&((priv_slotOne==PCI)||(priv_slotTwo==PCI)||(priv_slotThree==PCI)||(priv_slotFour==PCI))) ||
	
	((priv_graphiccrdSlot==ISA)&&((priv_slotOne==ISA)||(priv_slotTwo==ISA)||(priv_slotThree==ISA)||(priv_slotFour==ISA))) ||
	
	((priv_graphiccrdSlot==AGP)&&((priv_slotOne==AGP)||(priv_slotTwo==AGP)||(priv_slotThree==AGP)||(priv_slotFour==AGP))));




//graphic card type and graphic card slot binding:
	((GRAPHIC_CARD=="AsusAGPV3400TNTmTVInTVOut"&&priv_graphiccrdSlot==AGP)
	||
	(GRAPHIC_CARD=="CreativeLabsGraphicsBlasterRivaTNT"&&priv_graphiccrdSlot==AGP)
	||
	(GRAPHIC_CARD=="DiamondViper770"&&priv_graphiccrdSlot==AGP));


//ram capacity checks
(((priv_ramcap==0) && ((priv_ram1Exist + priv_ram2Exist + priv_ram3Exist + priv_ram4Exist) == 0) ||
((priv_ramcap==1) && ((priv_ram1Exist==1) && ((priv_ram2Exist+priv_ram3Exist+priv_ram4Exist) == 0))) ||
((priv_ramcap==2) && (priv_ram1Exist == 1) && ((priv_ram2Exist + priv_ram3Exist + priv_ram4Exist) == 0))) ||
((priv_ramcap==2) && ((priv_ram1Exist + priv_ram2Exist)==2) && ((priv_ram3Exist + priv_ram4Exist) == 0))) ||
((priv_ramcap==3) && (priv_ram1Exist== 1) && ((priv_ram2Exist+priv_ram3Exist+priv_ram4Exist) == 0)) ||
((priv_ramcap==3) && ((priv_ram1Exist + priv_ram2Exist)==2) && ((priv_ram3Exist+priv_ram4Exist) == 0)) ||
((priv_ramcap==3) && ((priv_ram1Exist + priv_ram2Exist + priv_ram3Exist) == 3) && (priv_ram4Exist == 0)) ||

((priv_ramcap==4) && (priv_ram1Exist==1) && ((priv_ram2Exist+priv_ram3Exist+priv_ram4Exist) == 0)) ||
((priv_ramcap==4) && ((priv_ram1Exist+priv_ram2Exist)==2) && ((priv_ram3Exist+priv_ram4Exist) == 0)) ||
((priv_ramcap==4) && ((priv_ram1Exist+priv_ram2Exist + priv_ram3Exist)==3) && (priv_ram4Exist == 0)) ||
((priv_ramcap==4) && ((priv_ram1Exist + priv_ram2Exist + priv_ram3Exist + priv_ram4Exist) == 4));

//ram block counter variables:
(((RAM1=="NoRAMBlock")&&(priv_ram1Exist==0))|| ((RAM1!="NoRAMBlock")&&(priv_ram1Exist==1)));
(((RAM2=="NoRAMBlock")&&(priv_ram2Exist==0))|| ((RAM2!="NoRAMBlock")&&(priv_ram2Exist==1)));
(((RAM3=="NoRAMBlock")&&(priv_ram3Exist==0))|| ((RAM3!="NoRAMBlock")&&(priv_ram3Exist==1)));
(((RAM4=="NoRAMBlock")&&(priv_ram4Exist==0))|| ((RAM4!="NoRAMBlock")&&(priv_ram4Exist==1)));


PC_RAM_CAPACITY==(priv_ram1Cap+priv_ram2Cap+priv_ram3Cap+priv_ram4Cap);


HARDDISK1 != "Noharddisk";
RAM1 != "NoRAMBlock";



//pc rules 
	//make sure one can power up: //Cpu - rules:
	((priv_motherbrdCpuslot == Slot1) && (priv_processorCpuSlot == Slot1) ||
       
       (priv_motherbrdCpuslot == Socket7) && (priv_processorCpuSlot == Socket7) ||
       
       (priv_motherbrdCpuslot == SuperSocket7) && (priv_processorCpuSlot == SuperSocket7) ||
       
       (priv_motherbrdCpuslot == SlotA) && (priv_processorCpuSlot == SlotA)); 
       
       
       (((PC_CLOCK == "P500MHz")&&(priv_processoFreq=="P500MHz"))||
	((PC_CLOCK == "P600MHz")&&(priv_processoFreq=="P600MHz"))||
	((PC_CLOCK == "P700MHz")&&(priv_processoFreq=="P700MHz"))||
	((PC_CLOCK == "P800MHz")&&(priv_processoFreq=="P800MHz")));

       
       (((priv_processoFreq =="P500MHz") && 
       	((priv_mincpufreq !="P600MHz" && priv_mincpufreq !="P700MHz") && (priv_mincpufreq !="P800MHz")  
              && (priv_maxCpufreq =="P500MHz") || (priv_maxCpufreq =="P600MHz") || (priv_maxCpufreq =="P700MHz") || (priv_maxCpufreq =="P800MHz"))) ||
               
       ((priv_processoFreq =="P600MHz") && 
       	((priv_mincpufreq !="P700MHz") && (priv_mincpufreq !="P800MHz")  
      		&&(priv_maxCpufreq !="P500MHz"))) ||
      
       ((priv_processoFreq =="P700MHz") &&
       	((priv_mincpufreq !="P800MHz")
              && (priv_maxCpufreq !="P500MHz") && (priv_maxCpufreq !="P600MHz") )) ||
              
       ((priv_processoFreq =="P800MHz") && 
       	(priv_maxCpufreq =="P800MHz")));