Testes do KEMS em Lote

De Wiki DAINF
(Diferença entre revisões)
(→CPU)
(→TODO: Exemplos de sequencias de testes para o KEMS v. 0.9)
 
(14 edições intermediárias de 2 usuários não apresentadas)
Linha 6: Linha 6:
 
== Como descobrir a configuração da máquina usada para testes no Linux ==
 
== 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 ===
 
=== CPU ===
Linha 21: Linha 33:
 
  stepping : 2
 
  stepping : 2
 
  '''cpu MHz : 1800.204'''
 
  '''cpu MHz : 1800.204'''
−
  cache size : 512 KB
+
  '''cache size : 512 KB'''
 
  fdiv_bug : no
 
  fdiv_bug : no
 
  hlt_bug : no
 
  hlt_bug : no
Linha 33: Linha 45:
 
  bogomips : 3602.35
 
  bogomips : 3602.35
  
−
== Memória ==
+
=== Memória ===
  
 
* Comando: cat /proc/meminfo
 
* Comando: cat /proc/meminfo
Linha 40: Linha 52:
  
 
  adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/meminfo  
 
  adolfo@vonneumann:~/KEMS/kems.export$ cat /proc/meminfo  
−
  MemTotal:      508596 kB
+
  '''MemTotal:      508596 kB'''
 
  (...)
 
  (...)
 
  VmallocChunk:  517824 kB
 
  VmallocChunk:  517824 kB
Linha 55: Linha 67:
  
 
* Para deixar em background (e assim poder deslogar e deixar rodando):
 
* Para deixar em background (e assim poder deslogar e deixar rodando):
−
  java -jar kems.jar <arquivo.seq> > results.tex &
+
  nohup java -jar kems.jar <arquivo.seq> > results.tex &
  
 
* Neste caso, acompanhar a execução do processo encontrando-o em  
 
* Neste caso, acompanhar a execução do processo encontrando-o em  
Linha 63: Linha 75:
 
ou
 
ou
 
  tail -f [results.tex]
 
  tail -f [results.tex]
 +
 +
= Como elaborar sequencias de testes =
 +
 +
Basta editar o arquivo .seq:
 +
 +
  nano teste.lfi.seq
 +
<br />
 +
E selecionar as famílias a serem provadas em '<strong>problems</strong>', escolher as estratégias à serem usadas em <strong>strategies</strong>, e os comparadores em <strong>comparators</strong>:
 +
 +
  parser=satlfiinconsdef
 +
  saveOrigin=true
 +
  discardClosedBranches=false
 +
  saveDiscardedBranches=false
 +
  times=1
 +
  timeLimit=10
 +
 +
  <strong>problems</strong>=
 +
  problems/generated/lfiProblems/family5/family5_05.prove
 +
  problems/generated/lfiProblems/family5/family5_10.prove
 +
  problems/generated/lfiProblems/family5/family5_15.prove
 +
 +
  <strong>strategies</strong>=
 +
  C1SimpleStrategy
 +
 +
  <strong>comparators</strong>=
 +
  InsertionOrderComparator
 +
  ReverseInsertionOrderComparator
 +
  #AndComparator
 +
 +
== Como decidir quantas vezes rodar cada caso ==
 +
 +
Ao editar o arquivo .seq:
 +
 +
  nano teste.lfi.seq
 +
<br />
 +
Adicionar o número de vezes em '<strong>times</strong>' (no caso esta como 1):
 +
 +
  parser=satlfiinconsdef
 +
  saveOrigin=true
 +
  discardClosedBranches=false
 +
  saveDiscardedBranches=false
 +
  <strong>times</strong>=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
 +
<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