Testes do KEMS em Lote
De Wiki DAINF
(Diferença entre revisões)
(→Como descobrir a configuração da máquina usada para testes no Linux) |
(→TODO: Exemplos de sequencias de testes para o KEMS v. 0.9) |
||
(11 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. | + | 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 34: | Linha 45: | ||
bogomips : 3602.35 | bogomips : 3602.35 | ||
− | == Memória == | + | === Memória === |
* Comando: cat /proc/meminfo | * Comando: cat /proc/meminfo | ||
Linha 56: | 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 64: | 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