Testes do KEMS em Lote

De Wiki DAINF

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
Ferramentas pessoais