Testes do KEMS em Lote
De Wiki DAINF
(Diferença entre revisões)
(→TODO: Como elaborar sequencias de testes) |
(→TODO: Exemplos de sequencias de testes para o KEMS v. 0.9) |
||
| (2 edições intermediárias de um usuário não apresentadas) | |||
| Linha 82: | Linha 82: | ||
nano teste.lfi.seq | nano teste.lfi.seq | ||
<br /> | <br /> | ||
| − | E selecionar as famílias a serem provadas em '<strong>problems</strong>': | + | 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 | parser=satlfiinconsdef | ||
| Linha 96: | Linha 96: | ||
problems/generated/lfiProblems/family5/family5_15.prove | problems/generated/lfiProblems/family5/family5_15.prove | ||
| − | strategies= | + | <strong>strategies</strong>= |
C1SimpleStrategy | C1SimpleStrategy | ||
| − | comparators= | + | <strong>comparators</strong>= |
InsertionOrderComparator | InsertionOrderComparator | ||
ReverseInsertionOrderComparator | ReverseInsertionOrderComparator | ||
#AndComparator | #AndComparator | ||
| − | == | + | == Como decidir quantas vezes rodar cada caso == |
Ao editar o arquivo .seq: | Ao editar o arquivo .seq: | ||
| Linha 119: | Linha 119: | ||
timeLimit=10 | timeLimit=10 | ||
| − | + | problems= | |
problems/generated/lfiProblems/family5/family5_05.prove | problems/generated/lfiProblems/family5/family5_05.prove | ||
problems/generated/lfiProblems/family5/family5_10.prove | problems/generated/lfiProblems/family5/family5_10.prove | ||
| Linha 132: | Linha 132: | ||
#AndComparator | #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
