Testes do KEMS em Lote

De Wiki DAINF
(Diferença entre revisões)
(→Como elaborar sequencias de testes)
(→TODO: Exemplos de sequencias de testes para o KEMS v. 0.9)
 
Linha 132: Linha 132:
 
   #AndComparator
 
   #AndComparator
  
−
= TODO: Exemplos de sequencias de testes para o KEMS v. 0.9=
+
= Exemplos de sequencias de testes para o KEMS v. 0.9=
 +
 
 +
  nano testes.lfi.seq
 +
<br />
 +
 
 +
  parser=satlfiinconsdef
 +
  saveOrigin=true
 +
  discardClosedBranches=false
 +
  saveDiscardedBranches=false
 +
  times=5
 +
  timeLimit=600
 +
 
 +
  problems=
 +
  problems/generated/lfiProblems/family5/family5_05.prove
 +
  problems/generated/lfiProblems/family5/family5_10.prove
 +
  problems/generated/lfiProblems/family5/family5_15.prove
 +
 
 +
  strategies=
 +
  C1SimpleStrategy
 +
  #ConfigurableSimpleStrategy
 +
  #MBCSimpleStrategy
 +
  #MBCConfigurableSimpleStrategy
 +
  #MBCSimpleWithOptionalRulesStrategy
 +
  #MCISimpleStrategy
 +
  #MCIConfigurableSimpleStrategy
 +
  #MCISimpleWithOptionalRulesStrategy
 +
  #MemorySaverStrategy
 +
  #SimpleStrategy
 +
  #BackjumpingSimpleStrategy
 +
  #LearningSimpleStrategy
 +
  #NewLearningSimpleStrategy
 +
 
 +
  comparators=
 +
  AndComparator
 +
  ConsistencyComplexityComparator
 +
  ComplexitySignedFormulaComparator
 +
  ConnectiveSignedFormulaComparator
 +
  ISignedFormulaComparator
 +
  InsertionOrderSignedFormulaComparator
 +
  InsertionOrderComparator
 +
  NormalFormulaOrderSignedFormulaComparator
 +
  ReverseFormulaOrderSignedFormulaComparator
 +
  ReverseInsertionOrderSignedFormulaComparator
 +
  ReverseInsertionOrderComparator
 +
  SignSignedFormulaComparator
 +
  #BiimpliesComparator
 +
  #XorComparato

Edição atual tal como 10h25min de 11 de novembro de 2009

Tabela de conteúdo

Configuração

  • Máquina: xue.dainf.ct.utfpr.edu.br
  • Servidor git

Como descobrir a configuração da máquina usada para testes no Linux

Em destaque nas linha abaixo os itens mais importantes. Ver mais em http://www.linux.com/archive/feature/126718?theme=print

Sistema Operacional

  • Comando: cat /proc/version
  • Exemplo: 
cat /proc/version 
Linux version 2.6.18-4-486 (Debian 2.6.18.dfsg.1-12etch2) (dannf@debian.org) (gcc version 4.1.2 20061115 (prerelease) (Debian 4.1.1-21)) #1 Wed May 9 22:23:40 UTC 2007


Ou uname -a

CPU

  • Comando: cat /proc/cpuinfo
  • Exemplo: 
adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/cpuinfo 
processor	: 0
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 47
model name	: AMD Athlon(tm) 64 Processor 3000+
stepping	: 2
cpu MHz		: 1800.204
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 syscall nx mmxext fxsr_opt lm 3dnowext 3dnow pni lahf_lm ts fid vid ttp tm stc
bogomips	: 3602.35

Memória

  • Comando: cat /proc/meminfo
  • Exemplo: 
adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/meminfo 
MemTotal:       508596 kB
(...)
VmallocChunk:   517824 kB

Roteiro

  • Editar arquivo de sequencia <arquivo.seq>.
  • Executar da seguinte forma: 
java -jar kems.jar <arquivo.seq>
  • Para direcionar para arquivo: 
java -jar kems.jar <arquivo.seq> > [results.tex]
  • Para deixar em background (e assim poder deslogar e deixar rodando): 
nohup java -jar kems.jar <arquivo.seq> > results.tex &
  • Neste caso, acompanhar a execução do processo encontrando-o em 
ps -aux | grep java

ou 

top

ou 

tail -f [results.tex]

Como elaborar sequencias de testes

Basta editar o arquivo .seq: 

  nano teste.lfi.seq


E selecionar as famílias a serem provadas em 'problems', escolher as estratégias à serem usadas em strategies, e os comparadores em comparators: 

  parser=satlfiinconsdef
  saveOrigin=true
  discardClosedBranches=false
  saveDiscardedBranches=false
  times=1
  timeLimit=10

  problems=
  problems/generated/lfiProblems/family5/family5_05.prove
  problems/generated/lfiProblems/family5/family5_10.prove
  problems/generated/lfiProblems/family5/family5_15.prove

  strategies=
  C1SimpleStrategy

  comparators=
  InsertionOrderComparator
  ReverseInsertionOrderComparator
  #AndComparator

Como decidir quantas vezes rodar cada caso

Ao editar o arquivo .seq: 

  nano teste.lfi.seq


Adicionar o número de vezes em 'times' (no caso esta como 1): 

  parser=satlfiinconsdef
  saveOrigin=true
  discardClosedBranches=false
  saveDiscardedBranches=false
  times=1
  timeLimit=10

  problems=
  problems/generated/lfiProblems/family5/family5_05.prove
  problems/generated/lfiProblems/family5/family5_10.prove
  problems/generated/lfiProblems/family5/family5_15.prove

  strategies=
  C1SimpleStrategy

  comparators=
  InsertionOrderComparator
  ReverseInsertionOrderComparator
  #AndComparator

Exemplos de sequencias de testes para o KEMS v. 0.9

 nano testes.lfi.seq



 parser=satlfiinconsdef
 saveOrigin=true
 discardClosedBranches=false
 saveDiscardedBranches=false
 times=5
 timeLimit=600

 problems=
 problems/generated/lfiProblems/family5/family5_05.prove
 problems/generated/lfiProblems/family5/family5_10.prove
 problems/generated/lfiProblems/family5/family5_15.prove

 strategies=
 C1SimpleStrategy
 #ConfigurableSimpleStrategy
 #MBCSimpleStrategy
 #MBCConfigurableSimpleStrategy
 #MBCSimpleWithOptionalRulesStrategy
 #MCISimpleStrategy
 #MCIConfigurableSimpleStrategy
 #MCISimpleWithOptionalRulesStrategy
 #MemorySaverStrategy
 #SimpleStrategy
 #BackjumpingSimpleStrategy
 #LearningSimpleStrategy
 #NewLearningSimpleStrategy

 comparators=
 AndComparator
 ConsistencyComplexityComparator
 ComplexitySignedFormulaComparator
 ConnectiveSignedFormulaComparator
 ISignedFormulaComparator
 InsertionOrderSignedFormulaComparator
 InsertionOrderComparator
 NormalFormulaOrderSignedFormulaComparator
 ReverseFormulaOrderSignedFormulaComparator
 ReverseInsertionOrderSignedFormulaComparator
 ReverseInsertionOrderComparator
 SignSignedFormulaComparator
 #BiimpliesComparator
 #XorComparato
Obtida de "http://dainf.ct.utfpr.edu.br/wiki/index.php?title=Testes_do_KEMS_em_Lote&oldid=2611"
Ferramentas pessoais